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 123 articles , 1 standard article )
Showing results 1 to 20 of 123.
Sorted by year (- Kojima, Kensuke; Imanishi, Akifumi; Igarashi, Atsushi: Automated verification of functional correctness of race-free GPU programs (2018)
- 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)
- Jonáš, Martin; Strejček, Jan: Solving quantified bit-vector formulas using binary decision diagrams (2016)
- Selsam, Daniel; de Moura, Leonardo: Congruence closure in intensional type theory (2016)
- Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: Decision procedures for flat array properties (2015)
- Bonacina, Maria Paola; Johansson, Moa: Interpolation systems for ground proofs in automated deduction: a survey (2015)
- Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
- Grechanik, S. A.: Proving properties of functional programs by equality saturation (2015)
- Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha: Search-space partitioning for parallelizing SMT solvers (2015)
- Jaroschek, Maximilian; Dobal, Pablo Federico; Fontaine, Pascal: Adapting real quantifier elimination methods for conflict set computation (2015)
- David R. Cok: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse (2014) arXiv
- Kuncak, Viktor: Verifying and synthesizing software with recursive functions (invited contribution) (2014)
- Filli^atre, Jean-Christophe: One logic to use them all (2013)
- Leino, K. Rustan M.: Automating theorem proving with SMT (2013)