Publications : Claire Dross
Back[9]  Clément Fumex, Claire Dross, Jens Gerlach, and Claude Marché. Specification and proof of highlevel functional properties of bitlevel programs. In Sanjai Rayadurgam and Oksana Tkachuk, editors, 8th NASA Formal Methods Symposium, volume 9690 of Lecture Notes in Computer Science, pages 291306, Minneapolis, MN, USA, June 2016. Springer. [ bib  full text on HAL ] 
[8] 
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Adding decision procedures to SMT solvers using axioms with
triggers.
Journal of Automated Reasoning, 56(4):387457, 2016.
[ bib 
full text on HAL ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of builtin theories such as congruence, linear arithmetic, arrays, and bitvectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a firstorder axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle firstorder logic and are included in the SMTLIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a onetime development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the AltErgo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a featurerich axiomatization of doublylinked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doublylinked lists.

[7]  Claire Dross, Clément Fumex, Jens Gerlach, and Claude Marché. Highlevel functional properties of bitlevel programs: Formal specifications and automated proofs. Research Report 8821, Inria, December 2015. [ bib  full text on HAL ] 
[6]  Claire Dross. Generic Decision Procedures for Axiomatic FirstOrder Theories. Thèse de doctorat, Université ParisSud, April 2014. [ bib  full text on HAL ] 
[5] 
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Adding decision procedures to SMT solvers using axioms with
triggers.
Submitted, 2013.
[ bib 
full text on HAL 
.pdf ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of builtin theories such as congruence, linear arithmetic, arrays, and bitvectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a firstorder axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle firstorder logic and are included in the SMTLIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a onetime development effort. We believe that this effort is not greater than that of adding a single decision procedure to the same SMT solver. We have implemented the proposed extension in the AltErgo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a featurerich axiomatization of doublylinked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doublylinked lists.

[4] 
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Reasoning with triggers.
Research Report RR7986, INRIA, June 2012.
[ bib 
full text on HAL 
.pdf ]
SMT solvers can decide the satisfiability of ground formulas modulo a combination of builtin theories. Adding a builtin theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using firstorder formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures. In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of firstorder axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate on two examples, how such proofs can be achieved in our formalism. Keywords: Quantifiers, Triggers, SMT Solvers, Theories 
[3]  Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, Manchester, UK, 2012. LORIA. [ bib ] 
[2]  Johannes Kanig, Edmond Schonberg, and Claire Dross. HiLite: the convergence of compiler technology and program verification. In Ben Brosgol, Jeff Boleng, and S. Tucker Taft, editors, Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT '12, pages 2734, Boston, USA, 2012. ACM Press. [ bib ] 
[1] 
Claire Dross, JeanChristophe Filliâtre, and Yannick Moy.
Correct Code Containing Containers.
In 5th International Conference on Tests and Proofs (TAP'11),
volume 6706 of Lecture Notes in Computer Science, pages 102118,
Zurich, June 2011. Springer.
[ bib 
full text on HAL 
.pdf ]
For critical software development, containers such as lists, vectors, sets or maps are an attractive alternative to adhoc data structures based on pointers. As standards like DO178C put formal verification and testing on an equal footing, it is important to give users the ability to apply both to the verification of code using containers. In this paper, we present a definition of containers whose aim is to facilitate their use in certified software, using modern proof technology and novel specification languages. Correct usage of containers and userprovided correctness properties can be checked either by execution during testing or by formal proof with an automatic prover. We present a formal semantics for containers and an axiomatization of this semantics targeted at automatic provers. We have proved in Coq that the formal semantics is consistent and that the axiomatization thereof is correct.

Back
This page was generated by bibtex2html.