Publications

[ PMR12b ] full text
O. Ponsini, C. Michel, M. Rueher, Combining Constraint Programming and Abstract Interpretation for Value Analysis of Floating-point Programs, 4th Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA'2012), Canada, April 2012.
[ PMR12 ] full text
O. Ponsini, C. Michel, M. Rueher, Refining abstract interpretation based value analysis with constraint programming techniques, International Conference on Principles and Practice of Constraint Programming (CP'2012), Canada, October 2012.
[ CLVPMR12b ] full text
H. Collavizza, N. Le Vinh, O. Ponsini, M. Rueher, A. Rollet, Constraint-Based BMC: A Backjumping Strategy, International Journal on Software Tools for Technology Transfer (STTT), August 2012.
[ CLVPMR12 ] full text
H. Collavizza, N. Le Vinh, O. Ponsini, M. Rueher, A. Rollet, The Flasher Manager Benchmarks, HAL, July 2012.
[ PMR11b ] full text
O. Ponsini, C. Michel, M. Rueher, Utilisation de solveurs de contraintes pour réduire les approximations produites par interprétation abstraite, Septièmes Journées Francophones de Programmation par Contraintes (JFPC'2011), France, June 2011.
[ PMR11 ] full text
O. Ponsini, C. Michel, M. Rueher, Refining Abstract Interpretation-based Approximations with a Floating-point Constraint Solver, 4th International Workshop on Numerical Software Verification (NSV'2011), USA, July 2011.
[ PCFMR10 ] full text
O. Ponsini, H. Collavizza, C. Fédèle, C. Michel, M. Rueher, Automatic Verification of Loop Invariants, proceedings of the 26th IEEE International Conference on Software Maintenance (ICSM'2010), Romania, September 2010.
[ GHPS09 ] link to full text
H. Garavel, C. Helmstetter, O. Ponsini, W. Serwe, Verification of an Industrial SystemC/TLM Model using LOTOS and CADP, proceedings of the 7th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2009), USA, July 2009.
[ HP08 ] link to full text
C. Helmstetter, O. Ponsini, A Comparison of Two SystemC/TLM Semantics for Formal Verification, proceedings of the 6th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2008), USA, June 2008.
[ PS08 ] link to full text
O. Ponsini, W. Serwe, A Schedulerless Semantics of TLM Models Written in SystemC via Translation into LOTOS, proceedings of the 15th International Symposium on Formal Methods (FM'08), Finland, May 2008.
[ PF06a ] full text
O. Ponsini, C. Fédèle, Mutable Lists and Call-by-Reference with SOSSubC, WSEAS Transactions on computers, 5(9):1942--1949, 2006.
[ PF06b ]
O. Ponsini, C. Fédèle, Towards verification of SubC programs with side effects, proceedings of the 10th WSEAS Int. Conf. on Computers, Greece, July 2006
[ Pon05 ] (in french) full text + slides
O. Ponsini, Des programmes impératifs vers la logique équationnelle pour la vérification, Thèse de Doctorat, soutenue le 24 novembre 2005
[ PF05 ] full text
O. Ponsini, C. Fédèle, Mutable lists and call-by-reference in equational logic, Technical Report 2005
[ PFK04 ] full text
O. Ponsini, C. Fédèle, E. Kounalis, Rewriting of imperative programs into logical equations, Science of Computer Programming, 56(3):363–401, June 2005
[ PFK03 ] full text
O. Ponsini, C. Fédèle, E. Kounalis, Automating Proof of C-- Programs, an extended version of [ PFK02 ], 2003, unpublished
[ Pon02 ] (in french) full text
O. Ponsini, Réécriture de programmes C-- en équations logiques, proceedings of the 11th Journées Francophones de Programmation Logique et Programmation par Contraintes, France, May 2002
[ PFK02 ] full text + slides
O. Ponsini, C. Fédèle, E. Kounalis, SOS C-- : A System for Interpreting Operational Semantics of C-- programs, proceedings of the 20th IASTED International Multi-Conference on Applied Informatics, Austria, February 2002