5 citations · 7 across the 5 of their papers we have counts for
6 papers
Using Program Synthesis for Program Analysis
Cristina David, Daniel Kroening, Matt Lewis
In this paper, we identify a fragment of second-order logic with restricted quantification that is expressive enough to capture numerous static analysis problems (e.g. safety provi…
Danger Invariants
Cristina David, Daniel Kroening, Matt Lewis
Static analysers search for overapproximating proofs of safety commonly known as safety invariants. Fundamentally, such analysers summarise traces into sets of states, thus trading…
Proving Safety with Trace Automata and Bounded Model Checking
Daniel Kroening, Matt Lewis, Georg Weissenbacher
Loop under-approximation is a technique that enriches C programs with additional branches that represent the effect of a (limited) range of loop iterations. While this technique ca…
Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
Cristina David, Daniel Kroening, Matt Lewis
Proving program termination is typically done by finding a well-founded ranking function for the program states. Existing termination provers typically find ranking functions using…
Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs
Cristina David, Daniel Kroening, Matt Lewis
This paper shows that it is possible to reason about the safety and termination of programs handling potentially cyclic, singly-linked lists using propositional reasoning even when…
Second-Order Propositional Satisfiability
Cristina David, Daniel Kroening, Matt Lewis
Fundamentally, every static program analyser searches for a proof through a combination of heuristics providing candidate solutions and a candidate validation technique. Essentiall…