2 citations · 2 across the 3 of their papers we have counts for
3 papers · 1 filter
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…