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 113 articles , 1 standard article )
Showing results 1 to 20 of 113.
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)
- Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: Decision procedures for flat array properties (2015)
- Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
- Bonacina, Maria Paola; Johansson, Moa: Interpolation systems for ground proofs in automated deduction: a survey (2015)
- Grechanik, S.A.: Proving properties of functional programs by equality saturation (2015)
- 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)
- 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)
- Shved, P.E.; Mutilin, V.S.; Mandrykin, M.U.: Experience of improving the BLAST static verification tool (2012)
- Thamsborg, Jacob; Birkedal, Lars; Yang, Hongseok: Two for the price of one: lifting separation logic assertions (2012)
- Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
- Bonacina, Maria Paola; Lynch, Christopher A.; de Moura, Leonardo: On deciding satisfiability by theorem proving with speculative inferences (2011)