Static Analysis and Verification of Aerospace Software by Abstract Interpretation, AIAA, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00528611
Solving Existentially Quantified Horn Clauses, CAV, pp.869-882, 2013. ,
DOI : 10.1007/978-3-642-39799-8_61
Liveness Checking as Safety Checking, Electronic Notes in Theoretical Computer Science, vol.66, issue.2, pp.160-177, 2002. ,
DOI : 10.1016/S1571-0661(04)80410-9
An Incremental Approach to Model Checking Progress Properties, FMCAD, pp.144-153, 2011. ,
Expectation Invariants for Probabilistic Program Loops as Fixed Points, SAS, pp.85-100, 2014. ,
DOI : 10.1007/978-3-319-10936-7_6
Proving that Programs Eventually do Something Good, POPL, pp.265-276, 2007. ,
DOI : 10.1145/1190215.1190257
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.7543
Reasoning About Nondeterminism in Programs, PLDI, pp.219-230, 2013. ,
Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, vol.277, issue.1-2, pp.77-102, 1997. ,
DOI : 10.1016/S0304-3975(00)00313-3
Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977. ,
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790
Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), Proceedings of 1994 IEEE International Conference on Computer Languages (ICCL'94), pp.95-112, 1994. ,
DOI : 10.1109/ICCL.1994.288389
An Abstract Interpretation Framework for Termination, POPL, pp.245-258, 2012. ,
Assigning Meanings to Programs, Proceedings of Symposium on Applied Mathematics, pp.19-32, 1967. ,
Apron: A Library of Numerical Abstract Domains for Static Analysis, CAV, pp.661-667, 2009. ,
DOI : 10.1007/978-3-642-02658-4_52
URL : https://hal.archives-ouvertes.fr/hal-00786354
A hierarchy of temporal properties, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing , PODC '87, pp.377-410, 1990. ,
DOI : 10.1145/41840.41857
Property Checking Driven Abstract Interpretation-Based Static Analysis, VMCAI, pp.56-69, 2003. ,
DOI : 10.1007/3-540-36384-X_8
Abstract Domains for Property Checking Driven Analysis of Temporal Properties, AMAST, pp.349-363, 2004. ,
DOI : 10.1007/978-3-540-27815-3_28
Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations, NSAD, pp.89-100, 2012. ,
DOI : 10.1016/j.entcs.2012.09.009
Transition invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pp.32-41, 2004. ,
DOI : 10.1109/LICS.2004.1319598
Transition Predicate Abstraction and Fair Termination, POPL, pp.132-144, 2005. ,
DOI : 10.1145/1232420.1232422
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.592.2631
The Abstract Domain of Segmented Ranking Functions, SAS, pp.43-62, 2013. ,
DOI : 10.1007/978-3-642-38856-9_5
URL : https://hal.archives-ouvertes.fr/hal-00925670
An Abstract Domain to Infer Ordinal-Valued Ranking Functions, ESOP, pp.412-431, 2014. ,
DOI : 10.1007/978-3-642-54833-8_22
URL : https://hal.archives-ouvertes.fr/hal-00925731
A Decision Tree Abstract Domain for Proving Conditional Termination, SAS, 2014. ,
DOI : 10.1007/978-3-319-10936-7_19
URL : https://hal.archives-ouvertes.fr/hal-01105221
Verification of concurrent programs: the automata-theoretic framework*, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.79-98, 1991. ,
DOI : 10.1016/0168-0072(91)90066-U