TRACER
TRACER: A Symbolic Execution Tool for Verification. TRACER is a verification tool based on symbolic execution for finite-state C sequential programs developed at National University of Singapore . TRACER attempts at building a finite symbolic execution tree which overapproximates the set of all concrete reachable states. If the error location cannot be reached from any symbolic path then the program is reported as safe. Otherwise, either the program may contain a bug or it may not terminate. TRACER reports a false alarm only if the theorem prover fails to prove a valid claim. The most innovative features of TRACER stem from how it tackles the two fundamental limitations of symbolic execution: exponential number of paths on the number of program branches, and infinite-length symbolic paths due to unbounded loops. TRACER computes interpolants (using weakest preconditions among other methods) from infeasible paths and integrates a novel counterexample-guided refinement phase within the symbolic execution process.
Keywords for this software
References in zbMATH (referenced in 12 articles )
Showing results 1 to 12 of 12.
Sorted by year (- Garcia-Contreras, Isabel; Morales, José F.; Hermenegildo, Manuel V.: Incremental and modular context-sensitive analysis (2021)
- Kafle, Bishoksan; Gallagher, John P.; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: An iterative approach to precondition inference using constrained Horn clauses (2018)
- Kafle, Bishoksan; Gallagher, John P.: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement (2017)
- Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
- Rusu, Vlad; Arusoaie, Andrei: Executing and verifying higher-order functional-imperative programs in Maude (2017)
- Aissat, Romain; Voisin, Frédéric; Wolff, Burkhart: Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths (2016)
- De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Proving correctness of imperative programs by linearizing constrained Horn clauses (2015)
- Gange, Graeme; Navas, Jorge A.; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: Horn clauses as an intermediate representation for program analysis and transformation (2015)
- De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Specialization with constrained generalization for software model checking (2013)
- Gange, Graeme; Navas, Jorge A.; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: Failure tabled constraint logic programming by interpolation (2013)
- De Angelis, Emanuele: Software model checking by program specialization (2012)
- Jaffar, Joxan; Murali, Vijayaraghavan; Navas, Jorge A.; Santosa, Andrew E.: TRACER: a symbolic execution tool for verification (2012)