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 105 articles , 1 standard article )
Showing results 1 to 20 of 105.
Sorted by year (- 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)
- 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)
- 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)
- Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
- Lynch, Christopher; Ta, Quang-Trung; Tran, Duc-Khanh: SMELS: satisfiability modulo equality with lazy superposition (2013)
- Promsky, A.V.: Experiments on self-applicability in the C-light verification system (2013)
- Brumley, Billy B.; Barbosa, Manuel; Page, Dan; Vercauteren, Frederik: Practical realisation and elimination of an ECC-related software bug attack (2012)
- Chin, Wei-Ngan; David, Cristina; Nguyen, Huu Hai; Qin, Shengchao: Automated verification of shape, size and bag properties via user-defined predicates in separation logic (2012)
- Cousot, Patrick; Cousot, Radhia; Mauborgne, Laurent: Theories, solvers and static analysis by abstract interpretation (2012)
- Echenim, Mnacho; Peltier, Nicolas: An instantiation scheme for satisfiability modulo theories (2012)
- Fuchs, Alexander; Goel, Amit; Grundy, Jim; Krstić, Sava; Tinelli, Cesare: Ground interpolation for the theory of equality (2012)
- Köksal, Ali Sinan; Kuncak, Viktor; Suter, Philippe: Constraints as control (2012) ioport
- Shved, P.E.; Mutilin, V.S.; Mandrykin, M.U.: Experience of improving the BLAST static verification tool (2012)