Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, vol.3, issue.2, pp.125-143, 1977. ,
DOI : 10.1109/TSE.1977.229904
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
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
Static Analysis and Verification of Aerospace Software by Abstract Interpretation, pp.1-38, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00528611
An Abstract Interpretation Framework for Termination, pp.245-258, 2012. ,
The Abstract Domain of Segmented Ranking Functions, 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, 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, pp.302-318, 2014. ,
DOI : 10.1007/978-3-319-10936-7_19
URL : https://hal.archives-ouvertes.fr/hal-01105221
Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation, pp.190-208, 2015. ,
DOI : 10.1007/978-3-662-46081-8_11
URL : https://hal.archives-ouvertes.fr/hal-01105238
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
Checking a Large Routine, Report of a Conference on High Speed Automatic Calculating Machines, pp.67-69, 1949. ,
Assigning meanings to programs, Proceedings of Symposium on Applied Mathematics, vol.19, pp.19-32, 1967. ,
DOI : 10.1090/psapm/019/0235771
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
Fixpoint Induction and Proofs of Program Properties, Machine Intelligence, vol.5, pp.59-78, 1969. ,
Static Determination of Dynamic Properties of Programs, Symposium on Programming, pp.106-130, 1976. ,
Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, pp.84-96, 1978. ,
DOI : 10.1145/512760.512770
The octagon abstract domain, Higher-Order and Symbolic Computation, vol.2477, issue.3, pp.31-100, 2006. ,
DOI : 10.1007/s10990-006-8609-1
Expectation Invariants for Probabilistic Program Loops as Fixed Points, pp.85-100, 2014. ,
DOI : 10.1007/978-3-319-10936-7_6
Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations, Electronic Notes in Theoretical Computer Science, vol.287, pp.89-100, 2012. ,
DOI : 10.1016/j.entcs.2012.09.009
Apron: A Library of Numerical Abstract Domains for Static Analysis, pp.661-667, 2009. ,
DOI : 10.1007/978-3-642-02658-4_52
URL : https://hal.archives-ouvertes.fr/hal-00786354
Efficient chaotic iteration strategies with widenings, pp.128-141, 1993. ,
DOI : 10.1007/BFb0039704
Conflict-Driven Conditional Termination, CAV (II), pp.271-286, 2015. ,
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, pp.144-153, 2011. ,
Transition Predicate Abstraction and Fair Termination, pp.132-144, 2005. ,
DOI : 10.1145/1232420.1232422
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.592.2631
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
The Size-Change Principle for Program Termination, pp.81-92, 2001. ,
Property Checking Driven Abstract Interpretation-Based Static Analysis, pp.56-69, 2003. ,
DOI : 10.1007/3-540-36384-X_8
Abstract Domains for Property Checking Driven Analysis of Temporal Properties, pp.349-363, 2004. ,
DOI : 10.1007/978-3-540-27815-3_28
Reasoning About Nondeterminism in Programs, pp.219-230, 2013. ,
Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM, vol.50, issue.5, pp.752-794, 2003. ,
DOI : 10.1145/876638.876643
Faster temporal reasoning for infinite-state programs, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.75-82, 2014. ,
DOI : 10.1109/FMCAD.2014.6987598
On Automation of CTL* Verification for Infinite-State Systems, CAV (I), pp.13-29, 2015. ,
DOI : 10.1007/978-3-319-21690-4_2
Proving Termination Starting from the End, pp.397-412, 2013. ,
DOI : 10.1007/978-3-642-39799-8_27
Policy Iteration-Based Conditional Termination and Ranking Functions, pp.453-471, 2014. ,
DOI : 10.1007/978-3-642-54013-4_25