39 citations · 73 across the 14 of their papers we have counts for
4 papers · 1 filter
AbPress: Flexing Partial-Order Reduction and Abstraction
Daniel Kroening, Subodh Sharma, Björn Wachter
Partial-order reduction (POR) and lazy abstraction with interpolants are two complementary techniques that have been successfully employed to make model checking tools for concurre…
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…