ESC/Java
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Harnessing rCOS for Tool Support —The CoCoME Experience
- A Hoare Logic for Call-by-Value Functional Programs
- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
- Formal Methods for Components and Objects
- A polymorphic intermediate verification language: design and logical encoding
- Korat
- JUnit
- Pex
- VCC
- ComFoRT
- JACK
- Boogie
- Atomizer
- SPEED
- CVC
- Amphion
- Coquet
- Galculator
- KeY
- RacerX
- MOPS
- VeriCool
- Sparkle
- LOOP
- TVLA
- jStar
- JCrasher
- Traffic 4
- CSPsim
- Mercator
- ASTREE
- CSSV
- FunArray
- Octagon
- VeriCon
- A shape graph logic and a shape system
- CacBDD
- Splint
- ExplainHoudini
- Houdini
- OpenJML
- BoogiePL
- MarQ
- StaRVOOrS
- CHESS
- CTrigger
- Rocksalt
- ASMKeY
- Zapato
- Nemerle
- Kami
- AutoProof
- Calysto
- Jass
- DynaMine
- Dava
- ANNA
- operational
- Cooperative bug isolation. Winning thesis of the 2005 ACM doctoral dissertation competition.
- Extending Model Checking with Dynamic Analysis
- ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
- Static contract checking with abstract interpretation
- scientific article; zbMATH DE number 5652074 (Why is no real title available?)
- A dynamic logic for deductive verification of multi-threaded programs
- Inferring sufficient conditions with backward polyhedral under-approximations
- scientific article; zbMATH DE number 1903353 (Why is no real title available?)
- A verifying compiler for a multi-threaded object-oriented language
- Model Checking Software
- Bugs, moles and skeletons: symbolic reasoning for software development
- Statically safe program generation with SafeGen
- Mathematics of Program Construction
- Valigator: A Verification Tool with Bound and Invariant Generation
- Verification, Model Checking, and Abstract Interpretation
- BDD
- JDD
- Concurrency bugs in multithreaded software: modeling and analysis using Petri nets
- Doomed program points
- Weakest pre-condition reasoning for Java programs with JML annotations
- SableJBDD
- Integration of verification methods for program systems
- Dual analysis for proving safety and finding bugs
- A system for compositional verification of asynchronous objects
- Modular verification of multithreaded programs
- Automated Technology for Verification and Analysis
- Modular verification of programs with effects and effects handlers
- Structural Abstraction of Software Verification Conditions
- Interpolant based decision procedure for quantifier-free Presburger arithmetic
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- SMT proof checking using a logical framework
- Programming Languages and Systems
- A mechanical analysis of program verification strategies
- Specification and verification challenges for sequential object-oriented programs
- Precondition inference from intermittent assertions and application to contracts on collections
- scientific article; zbMATH DE number 2087548 (Why is no real title available?)
- A proof outline logic for object-oriented programming
- E-matching for fun and profit
- Programming Languages and Systems
- Logical Interpretation: Static Program Analysis Using Theorem Proving
- ExplainHoudini: making Houdini inference transparent
This page was built for software: ESC/Java
