Predicate abstraction for software verification
By Cormac Flanagan, Shaz Qadeer. ACM-SIGACT Symposium on Principles of Programming Languages, 2002
332 citations recorded by the source corpus.
Subfields: Computational Theory and Mathematics, Information Systems, Software
View Paper: https://www.semanticscholar.org/paper/f4b5378de37dbc7521c9fd41216b77b3ab6f76b6
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Computational Theory and Mathematics
- Daniele Cono D'Elia
- Armando Solar-Lezama
- Wei-Ngan Chin
- Alvin Cheung
- Samuel Madden
- Greg Nelson
- Irene Finocchi
- Roberto Baldoni
In Information Systems
- Armando Solar-Lezama
- Wei-Ngan Chin
- Alvin Cheung
- Samuel Madden
- Greg Nelson
- Roberto Baldoni
- Patrick Maxim Rondon
- Corneliu Popeea
In Software
- Daniele Cono D'Elia
- Armando Solar-Lezama
- Wei-Ngan Chin
- Alvin Cheung
- Samuel Madden
- Greg Nelson
- Irene Finocchi
- Roberto Baldoni
Citations in the corpus
- Optimizing database-backed applications with query synthesis (2013, methodology): “There has been earlier work on automatically inferring loop invariants, such as using predicate refinement [14] or dynamic detection [13, 18].”
- Liquid types (2008, background): “Predicate abstraction has proven effective for path-sensitive verification of control-dominated properties of first-order imperative programs [3, 16, 11, 4, 29, 17].”
- Software model checking (2009, unknown): “In the worst case, the computation is exponential in the number of predicates, and several heuristics with better performance in practice have been proposed [Säıdi and Shankar 1999; Flanagan and Qadeer 2002].”
- Data Minimisation: A Language-Based Approach (2016, background): “To find the best invariant is a difficult problem and still an active field of research [12].”
- A Survey of Symbolic Execution Techniques (2016, background): “Predicate abstraction is a form of abstract interpretation over a domain constructed using a given set of predicates, and has been used to infer universally quantified loop invariants [46], which are useful when manipulating arrays.”
- Extended static checking for Java (2002, background): “to tackle some of the more significant sources of unsoundness, including loops (by loop invariant inference [18]) and modifies lists [34].”
- Inferring Disjunctive Postconditions (2006, methodology): “Methods for loop invariant inference include the induction-iteration approach [25] and approaches based on predicate abstraction [11, 17].”