SIMPLIFY
Extended static checking. This paper provides an overview of Extended Static Checking (ESC), a new technology that we have studied here at the Compaq (née Digital) Systems Research Center for much of the 1990s. We have implemented and experimented with two Extended Static Checkers, one for Modula-3, and another checker for Java. The aim of ESC is to increase software productivity by providing practical static checking tools for programmers. In general, static checking finds errors statically, that is, without running the program, and therefore can find errors earlier in the design process than dynamic checking such as testing. Since the cost of correcting an error is reduced if it is detected early, improved static checking has the potential to increase software productivity.
Keywords for this software
References in zbMATH (referenced in 141 articles , 1 standard article )
Showing results 1 to 20 of 141.
Sorted by year (- Fontaine, Pascal; Schurr, Hans-Jörg: Quantifier simplification by unification in SMT (2021)
- Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier: First-order automated reasoning with theories: when deduction modulo theory meets practice (2020)
- Neider, Daniel; Madhusudan, P.; Saha, Shambwaditya; Garg, Pranav; Park, Daejun: A learning-based approach to synthesizing invariants for incomplete verification engines (2020)
- Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
- Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan: Refutation-based synthesis in SMT (2019)
- Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
- Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
- Klebanov, Vladimir; Rümmer, Philipp; Ulbrich, Mattias: Automating regression verification of pointer programs by predicate abstraction (2018)
- Kojima, Kensuke; Imanishi, Akifumi; Igarashi, Atsushi: Automated verification of functional correctness of race-free GPU programs (2018)
- Reger, Giles; Suda, Martin; Voronkov, Andrei: Unification with abstraction and theory instantiation in saturation-based reasoning (2018)
- Barbosa, Haniel; Fontaine, Pascal; Reynolds, Andrew: Congruence closure with free variables (2017)
- Feldman, Yotam M. Y.; Padon, Oded; Immerman, Neil; Sagiv, Mooly; Shoham, Sharon: Bounded quantifier instantiation for checking inductive invariants (2017)
- Preiner, Mathias; Niemetz, Aina; Biere, Armin: Counterexample-guided model synthesis (2017)
- Reynolds, Andrew; King, Tim; Kuncak, Viktor: Solving quantified linear arithmetic by counterexample-guided instantiation (2017)
- Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark: Constraint solving for finite model finding in SMT solvers (2017)
- Wood, Tim; Drossopolou, Sophia; Lahiri, Shuvendu K.; Eisenbach, Susan: Modular verification of procedure equivalence in the presence of memory allocation (2017)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
- Galán, Francisco J.; Cañete-Valdeón, José M.: Synthesis of positive logic programs for checking a class of definitions with infinite quantification (2016)
- Hyvärinen, Antti E. J.; Marescotti, Matteo; Alt, Leonardo; Sharygina, Natasha: OpenSMT2: an SMT solver for multi-core and cloud computing (2016)