Software model checking
R Jhala, R Majumdar - ACM Computing Surveys (CSUR), 2009 - dl.acm.org
Software model checking Page 1 21 Software Model Checking RANJIT JHALA University of
California, San Diego and RUPAK MAJUMDAR University of California, Los Angeles We survey …
California, San Diego and RUPAK MAJUMDAR University of California, Los Angeles We survey …
ICE: A robust framework for learning invariants
We introduce ICE, a robust learning paradigm for synthesizing invariants, that learns using
examples, counter-examples, and implications, and show that it admits honest teachers and …
examples, counter-examples, and implications, and show that it admits honest teachers and …
Compositional shape analysis by means of bi-abduction
C Calcagno, D Distefano, P O'Hearn… - Proceedings of the 36th …, 2009 - dl.acm.org
This paper describes a compositional shape analysis, where each procedure is analyzed
independently of its callers. The analysis uses an abstract domain based on a restricted …
independently of its callers. The analysis uses an abstract domain based on a restricted …
Compositional shape analysis by means of bi-abduction
C Calcagno, D Distefano, PW O'hearn… - Journal of the ACM (JACM …, 2011 - dl.acm.org
The accurate and efficient treatment of mutable data structures is one of the outstanding
problem areas in automatic program verification and analysis. Shape analysis is a form of …
problem areas in automatic program verification and analysis. Shape analysis is a form of …
Inductive invariant generation via abductive inference
I Dillig, T Dillig, B Li, K McMillan - Acm Sigplan Notices, 2013 - dl.acm.org
This paper presents a new method for generating inductive loop invariants that are
expressible as boolean combinations of linear integer constraints. The key idea underlying …
expressible as boolean combinations of linear integer constraints. The key idea underlying …
Better quality in synthesis through quantitative objectives
Most specification languages express only qualitative constraints. However, among two
implementations that satisfy a given specification, one may be preferred to another. For …
implementations that satisfy a given specification, one may be preferred to another. For …
Static contract checking with abstract interpretation
M Fähndrich, F Logozzo - International conference on formal verification of …, 2010 - Springer
We present an overview of Clousot, our current tool to statically check CodeContracts.
CodeContracts enable a compiler and language-independent specification of Contracts …
CodeContracts enable a compiler and language-independent specification of Contracts …
A parametric segmentation functor for fully automatic and scalable array content analysis
P Cousot, R Cousot, F Logozzo - ACM SIGPLAN Notices, 2011 - dl.acm.org
We introduce FunArray, a parametric segmentation abstract domain functor for the fully
automatic and scalable analysis of array content properties. The functor enables a natural …
automatic and scalable analysis of array content properties. The functor enables a natural …
On solving universally quantified horn clauses
N Bjørner, K McMillan, A Rybalchenko - … 2013, Seattle, WA, USA, June 20 …, 2013 - Springer
Program proving can be viewed as solving for unknown relations (such as loop invariants,
procedure summaries and so on) that occur in the logical verification conditions of a …
procedure summaries and so on) that occur in the logical verification conditions of a …
Finding loop invariants for programs over arrays using a theorem prover
L Kovács, A Voronkov - International Conference on Fundamental …, 2009 - Springer
We present a new method for automatic generation of loop invariants for programs
containing arrays. Unlike all previously known methods, our method allows one to generate …
containing arrays. Unlike all previously known methods, our method allows one to generate …