19 citations · 33 across the 10 of their papers we have counts for
4 papers · 1 filter
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…
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…