Publications : Claire Dross
Retour[16]  Claire Dross and Johannes Kanig. Recursive data structures in spark. In Computer Aided Verification, 2020. [ bib ] 
[15]  GeorgesAxel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei Paskevich. Verification of programs with pointers in SPARK. In Formal Methods and Software Engineering (ICFEM), pages 5572, 2020. [ bib  DOI  full text on HAL ] 
[14]  GeorgesAxel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, and Andrei Paskevich. Verification of programs with pointers in SPARK. working paper https://hal.inria.fr/hal01936105, November 2018. [ bib  full text on HAL ] 
[13]  Claire Dross and Yannick Moy. Autoactive proof of redblack trees in spark. In NASA Formal Methods, 2017. [ bib ] 
[12]  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 ] 
[11]  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 ] 
[10] 
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.

[9]  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 ] 
[8]  Claire Dross. Generic Decision Procedures for Axiomatic FirstOrder Theories. Thèse de doctorat, Université ParisSud, 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 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.

[6] 
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 
[5]  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 ] 
[4]  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 ] 
[3] 
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.

[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 328344. 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 ObjectOriented 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 reestablished.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 postconditions 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 invariantbased reasoning.We also argue that even though encoding invariant protocols through methods' pre and postconditions 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 errorprone. Finally, we show that such encodings often cannot express properties over inaccessible objects, whereas an appropriate invariant protocol can handle them simply.

Retour
This page was generated by bibtex2html.