ESC/Java
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Refinement and verification in component-based model-driven design
- Solving quantified verification conditions using satisfiability modulo theories
- Integration of verification methods for program systems
- HOL-Boogie
- KeY-C
- JDD
- BDD
- Symstra
- Cogent
- jContractor
- rCOS
- SyncGen
- SafeGen
- LARCH
- SCOOP
- BLAST
- SPARK
- SLAM
- KRAKATOA
- Eiffel
- Daikon
- GeoSteiner
- JML
- Spec#
- Omnibus
- distcc
- Caduceus
- UCLID
- IsaWin
- SIMPLIFY
- Class invariants as abstract interpretation of trace semantics
- A type system for static and dynamic checking of C++ pointers
- Formal methods for smart cards: an experience report
- How the design of JML accommodates both runtime assertion checking and formal verification
- Generating error traces from verification-condition counterexamples
- UniTESK
- Weakest pre-condition reasoning for Java programs with JML annotations
- Source code verification of a secure payment applet
- Automatic software model checking via constraint logic
- Zap
- Bogor
- ESC4
- VCC
- Korat
- DART
- JUnit
- Pex
- Eclat
- A system for compositional verification of asynchronous objects
- Dual analysis for proving safety and finding bugs
- ComFoRT
- Boogie
- JACK
- Modular verification of programs with effects and effects handlers
- SPEED
- Atomizer
- Verifying Whiley programs with Boogie
- CVC
- VeriCool
- Sparkle
- TVLA
- Coquet
- RacerX
- Amphion
- KeY
- Galculator
- MOPS
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- LOOP
- Loop summarization using state and transition invariants
- jStar
- Cooperative bug isolation. Winning thesis of the 2005 ACM doctoral dissertation competition.
- Concurrency bugs in multithreaded software: modeling and analysis using Petri nets
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- A graph-based generic type system for object-oriented programs
- SMT proof checking using a logical framework
- Traffic 4
- The Daikon system for dynamic detection of likely invariants
- JCrasher
- Mercator
- CSPsim
- CSSV
- Octagon
- ASTREE
- FunArray
- A proof outline logic for object-oriented programming
- Dynamic inference of polymorphic lock types
- Model checking, testing and verification working together
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Highly dependable concurrent programming using design for verification
- Specification and verification challenges for sequential object-oriented programs
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Extended static checking
- VeriCon
- E-matching for fun and profit
- Programmed strategies for program verification
- Two for the price of one: lifting separation logic assertions
- Horn clause solvers for program verification
- Splint
This page was built for software: ESC/Java
