Publications : Claire Dross
Back[15] | Claire Dross and Johannes Kanig. Recursive data structures in spark. In Computer Aided Verification, 2020. [ bib ] |
[14] | Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei Paskevich. Verification of programs with pointers in SPARK. working paper https://hal.inria.fr/hal-01936105, November 2018. [ bib | full text on HAL ] |
[13] | Claire Dross and Yannick Moy. Auto-active proof of red-black trees in spark. In NASA Formal Methods, 2017. [ bib ] |
[12] | Clément Fumex, Claire Dross, Jens Gerlach, and Claude Marché. Specification and proof of high-level functional properties of bit-level programs. In Sanjai Rayadurgam and Oksana Tkachuk, editors, 8th NASA Formal Methods Symposium, volume 9690 of Lecture Notes in Computer Science, pages 291--306, Minneapolis, MN, USA, June 2016. Springer. [ bib | full text on HAL ] |
[11] |
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):387--457, 2016.
[ bib |
full text on HAL ]
SMT solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. 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 first-order 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 first-order logic and are included in the SMT-LIB 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 one-time 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 Alt-Ergo 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 feature-rich axiomatization of doubly-linked 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 doubly-linked lists. |
[10] | Claire Dross and Yannick Moy. Abstract software specifications and automatic proof of refinement. In 1st International Conference on Reliability, Safety and Security of Railway Systems, 2016. [ bib ] |
[9] | Claire Dross, Clément Fumex, Jens Gerlach, and Claude Marché. High-level functional properties of bit-level programs: Formal specifications and automated proofs. Research Report 8821, Inria, December 2015. [ bib | full text on HAL ] |
[8] | Claire Dross. Generic Decision Procedures for Axiomatic First-Order Theories. Thèse de doctorat, Université Paris-Sud, April 2014. [ bib | full text on HAL ] |
[7] |
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 built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. 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 first-order 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 first-order logic and are included in the SMT-LIB 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 one-time 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 Alt-Ergo 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 feature-rich axiomatization of doubly-linked 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 doubly-linked lists. |
[6] |
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich.
Reasoning with triggers.
Research Report RR-7986, INRIA, June 2012.
[ bib |
full text on HAL |
.pdf ]
SMT solvers can decide the satisfiability of ground formulas modulo a combination of built-in theories. Adding a built-in 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 first-order 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 first-order 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 |
[5] | Johannes Kanig, Edmond Schonberg, and Claire Dross. Hi-Lite: 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 27--34, Boston, USA, 2012. ACM Press. [ bib ] |
[4] | 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 ] |
[3] |
Claire Dross, Jean-Christophe 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 102--118,
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 ad-hoc data structures based on pointers. As standards like DO-178C 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 user-provided 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. |
[2] | Alexander J. Summers and Sophia Drossopoulou. Considerate reasoning and the composite design pattern. In Gilles Barthe and Manuel V. Hermenegildo, editors, VMCAI, volume 5944 of Lecture Notes in Computer Science, pages 328--344. Springer, 2010. [ bib ] |
[1] |
Alexander J. Summers, Sophia Drossopoulou, and Peter Müller.
The need for flexible object invariants.
In International Workshop on Aliasing, Confinement and Ownership
in Object-Oriented Programming, IWACO '09, New York, NY, USA, 2009.
Association for Computing Machinery.
[ bib |
DOI |
http ]
Specification and verification of object oriented programs usually features in some capacity the concept of an object invariant, used to describe the consistent states of an object. Unavoidably, an object's invariant will be broken at some points in its lifetime, and as a result, invariant protocols have been suggested, which prescribe the times at which object invariants may be broken, and the points at which they have to be re-established.The fact that currently available invariant protocols do not handle well some known examples, together with the fact that object invariants and invariant protocols can largely be encoded through methods' pre- and post- conditions has recently raised the question of whether they still have a role to play, or should be replaced by more explicit pre- and post-conditions for methods.In this paper we argue that invariant protocols express programmers' intuitions, lead to better design, allow more succinct specifications and proofs, and allow the expression of properties which involve many objects in a localised manner. In particular, the resulting verification conditions can be made simpler and more modular through the use of invariant-based reasoning.We also argue that even though encoding invariant protocols through methods' pre- and post-conditions is possible, such an encoding loses important information, and as a result makes specifications less explicit and program evolution (whereby the program evolves after the encoding has taken place) more error-prone. Finally, we show that such encodings often cannot express properties over inaccessible objects, whereas an appropriate invariant protocol can handle them simply. |
Back
This page was generated by bibtex2html.