Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016), p.887904, 2016. ,
DOI : 10.1007/978-3-662-49674-9_55
Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D, 2002. ,
URL : https://hal.archives-ouvertes.fr/inria-00528442
A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03, 2003. ,
DOI : 10.1145/780822.781153
URL : https://hal.archives-ouvertes.fr/hal-00128135
Abstract Interpretation with Alien Expressions and Heap Structures, p.147163, 2005. ,
DOI : 10.1007/978-3-540-30579-8_11
Modular Construction of Shape-Numeric Analyzers, Festschrift for Dave Schmidt. Festschrift for Dave Schmidt, 2013. ,
DOI : 10.1007/3-540-61739-6_53
URL : https://hal.archives-ouvertes.fr/hal-00926948
A policy iteration algorithm for computing xed points in static analysis of programs, Computer aided verication, p.462475, 2005. ,
Abstract interpretation: a unied lattice model for static analysis of programs by construction or approximation of xpoints, Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p.238252, 1977. ,
Abstract Interpretation Frameworks, Journal of Logic and Computation, vol.2, issue.4, p.511547, 1992. ,
DOI : 10.1093/logcom/2.4.511
A parametric segmentation functor for fully automatic and scalable array content analysis, Conference Record of the 38 th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011. ,
DOI : 10.1145/1926385.1926399
URL : https://hal.archives-ouvertes.fr/inria-00543874
Eciently computing static single assignment form and the control dependence graph, ACM Trans. Program. Lang. Syst, vol.13, issue.4, p.451490, 1991. ,
DOI : 10.1145/115372.115320
Recovering High-Level Conditions from Binary Programs, FM 2016: Formal Methods -21st International Symposium Proceedings, p.235253, 2016. ,
DOI : 10.1109/SP.2015.47
Static Contract Checking with Abstract Interpretation, Proceedings of the 2010 International Conference on Formal Verication of Object-oriented Software. pp. 1030. FoVeOOS'10, 2011. ,
DOI : 10.1007/978-3-540-79124-9_10
An Abstract Domain of Uninterpreted Functions, p.85103, 2016. ,
DOI : 10.1007/978-3-662-49122-5_4
Exploiting sparsity in dierence-bound matrices, Proceedings of the 23rd Static Analysis Symposium, 2016. ,
DOI : 10.1007/978-3-662-53413-7_10
Abstract acceleration in linear relation analysis, Science of Computer Programming, vol.93, p.125153, 2014. ,
DOI : 10.1016/j.scico.2013.09.016
URL : https://hal.archives-ouvertes.fr/hal-00785116
Static analysis of arithmetical congruences, International Journal of Computer Mathematics, vol.30, issue.3-4, p.165190, 1989. ,
DOI : 10.1145/29873.29875
A formallyveried c static analyzer, ACM SIGPLAN Notices, vol.50, issue.1, p.247259, 2015. ,
DOI : 10.1145/2775051.2676966
Ane relationships among variables of a program, Acta Informatica, vol.6, p.133151, 1976. ,
Frama-C: A software analysis perspective, Formal Aspects of Computing, vol.12, issue.1???2, p.573609, 2015. ,
DOI : 10.1007/11408901_21
Ecient weakest preconditions, Information Processing Letters, vol.93, issue.6, p.281288, 2005. ,
DOI : 10.1016/j.ipl.2004.10.015
URL : http://research.microsoft.com/pubs/70052/tr-2004-34.pdf
On the Relative Completeness of Bytecode Analysis Versus Source Code Analysis, 2008. ,
DOI : 10.1007/978-3-540-78791-4_14
Consistency in networks of relations, Artificial Intelligence, vol.8, issue.1, pp.99-118, 1977. ,
DOI : 10.1016/0004-3702(77)90007-8
Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics, Proc. of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES'06, 2006. ,
Symbolic Methods to Enhance the Precision of Numerical Abstract Domains, 2007. ,
DOI : 10.1007/11609773_23
Principles of program analysis, 1999. ,
DOI : 10.1007/978-3-662-03811-6
URL : http://www.seas.harvard.edu/courses/cs252/2011sp/slides/Lec11-AbstractInt.pdf
Design and implementation of sparse global analyses for c-like languages, Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation . pp. 229238. PLDI '12, 2012. ,
Polynomial Invariants by Linear Algebra, Automated Technology for Verication and Analysis -14th International Symposium, ATVA 2016 Proceedings, p.479494, 2016. ,
DOI : 10.1137/0201010
A structural approach to operational semantics, Tech. rep, 1981. ,
Precise and ecient static array bound checking for large embedded C programs, Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, p.231242, 2004. ,
DOI : 10.1145/996893.996869
URL : http://www.ic.arc.nasa.gov/m/pub/753h/0753%20(Venet).pdf
A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, 1994. ,
DOI : 10.1006/inco.1994.1093
URL : https://doi.org/10.1006/inco.1994.1093