ESC/Java
From MaRDI portal
swMATH7217MaRDI QIDQ19268FDOQ19268
Author name not available (Why is that?)
Official website: http://kindsoftware.com/products/opensource/ESCJava2/
Cited In (only showing first 100 items - show all)
- Loop summarization using state and transition invariants
- Verifying Heap-Manipulating Programs in an SMT Framework
- Tools and Algorithms for the Construction and Analysis of Systems
- Class invariants as abstract interpretation of trace semantics
- Formal methods for smart cards: an experience report
- Inferring Loop Invariants Using Postconditions
- Formalisation and implementation of an algorithm for bytecode verification of \(\@\)NonNull types
- SableJBDD
- Extended Static Checking by Calculation Using the Pointfree Transform
- Formal verification of a Java component using the RESOLVE framework
- Ghost signals: verifying termination of busy waiting
- Mathematics of Program Construction
- Programming Languages and Systems
- Programming Languages and Systems
- Dynamic inference of polymorphic lock types
- Efficient weakest preconditions
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- A relation-algebraic approach to the ``Hoare logic of functional dependencies
- Unit checking: symbolic model checking for a unit of code
- Automation of broad sanity test generation
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- BDD
- JDD
- Beyond contracts for concurrency
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Modular Safety Checking for Fine-Grained Concurrency
- A novel analysis space for pointer analysis and its application for bug finding
- Programmed strategies for program verification
- Interpolant Generation for UTVPI
- Collaborative verification and testing with explicit assumptions
- Horn clause solvers for program verification
- Fundamental Approaches to Software Engineering
- Matching logic: an alternative to Hoare/Floyd logic
- Bounded quantifier instantiation for checking inductive invariants
- Automatic software model checking via constraint logic
- An integrated approach to high integrity software verification
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Model checking, testing and verification working together
- Refinement and verification in component-based model-driven design
- Title not available (Why is that?)
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- A type system for static and dynamic checking of C++ pointers
- A Reachability Predicate for Analyzing Low-Level Software
- FM 2005: Formal Methods
- Atomizer: A dynamic atomicity checker for multithreaded programs
- Solving quantified verification conditions using satisfiability modulo theories
- Observational purity and encapsulation
- How the design of JML accommodates both runtime assertion checking and formal verification
- Generating error traces from verification-condition counterexamples
- Extending Model Checking with Dynamic Analysis
- A shape graph logic and a shape system
- Model Checking Software
- A verifying compiler for a multi-threaded object-oriented language
- Title not available (Why is that?)
- A dynamic logic for deductive verification of multi-threaded programs
- Verification, Model Checking, and Abstract Interpretation
- Weakest pre-condition reasoning for Java programs with JML annotations
- Doomed program points
- Integration of verification methods for program systems
- A system for compositional verification of asynchronous objects
- Modular verification of multithreaded programs
- Structural Abstraction of Software Verification Conditions
- Modular verification of programs with effects and effects handlers
- Programming Languages and Systems
- Specification and verification challenges for sequential object-oriented programs
- A mechanical analysis of program verification strategies
- Title not available (Why is that?)
- Programming Languages and Systems
- Frontiers of Combining Systems
- Logical Interpretation: Static Program Analysis Using Theorem Proving
- A proof outline logic for object-oriented programming
- Harnessing rCOS for Tool Support —The CoCoME Experience
- Formal Methods for Components and Objects
- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
- The Daikon system for dynamic detection of likely invariants
- Faster and more complete extended static checking for the Java modeling language
- Computer Aided Verification
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- On deciding satisfiability by theorem proving with speculative inferences
- Static contract checking with abstract interpretation
- HOL-Boogie
- KeY-C
- Inferring sufficient conditions with backward polyhedral under-approximations
- Cogent
- jContractor
- Symstra
- rCOS
- LARCH
- SafeGen
- SyncGen
- SCOOP
- BLAST
- KRAKATOA
- SLAM
- SPARK
- Eiffel
- Daikon
- GeoSteiner
This page was built for software: ESC/Java
