The following pages link to ESC/Java (Q19268):
Displaying 50 items.
- A relation-algebraic approach to the ``Hoare logic'' of functional dependencies (Q406457) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- A dynamic logic for deductive verification of multi-threaded programs (Q470007) (← links)
- Statically safe program generation with SafeGen (Q532402) (← links)
- Formalisation and implementation of an algorithm for bytecode verification of \(\@\)NonNull types (Q532427) (← links)
- Modular verification of multithreaded programs (Q557795) (← links)
- Doomed program points (Q633286) (← links)
- A shape graph logic and a shape system (Q744329) (← links)
- Formal verification of a Java component using the RESOLVE framework (Q831953) (← links)
- Ghost signals: verifying termination of busy waiting (Q832247) (← links)
- Efficient weakest preconditions (Q835051) (← links)
- Automation of broad sanity test generation (Q840076) (← links)
- Beyond contracts for concurrency (Q846113) (← links)
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) (Q861691) (← links)
- An integrated approach to high integrity software verification (Q861714) (← links)
- Observational purity and encapsulation (Q882452) (← links)
- Atomizer: A dynamic atomicity checker for multithreaded programs (Q924672) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- A novel analysis space for pointer analysis and its application for bug finding (Q988180) (← links)
- Refinement and verification in component-based model-driven design (Q1004291) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- Integration of verification methods for program systems (Q1040327) (← links)
- Class invariants as abstract interpretation of trace semantics (Q1749225) (← links)
- A type system for static and dynamic checking of C++ pointers (Q1767975) (← links)
- Formal methods for smart cards: an experience report (Q1776578) (← links)
- How the design of JML accommodates both runtime assertion checking and formal verification (Q1776585) (← links)
- Generating error traces from verification-condition counterexamples (Q1776586) (← links)
- Weakest pre-condition reasoning for Java programs with JML annotations (Q1881666) (← links)
- Source code verification of a secure payment applet (Q1881671) (← links)
- Automatic software model checking via constraint logic (Q1887740) (← links)
- A system for compositional verification of asynchronous objects (Q1951610) (← links)
- Dual analysis for proving safety and finding bugs (Q1951646) (← links)
- Modular verification of programs with effects and effects handlers (Q1996433) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- Loop summarization using state and transition invariants (Q2248058) (← links)
- Cooperative bug isolation. Winning thesis of the 2005 ACM doctoral dissertation competition. (Q2371959) (← links)
- Concurrency bugs in multithreaded software: modeling and analysis using Petri nets (Q2393141) (← links)
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (Q2402555) (← links)
- A graph-based generic type system for object-oriented programs (Q2418638) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- The Daikon system for dynamic detection of likely invariants (Q2463543) (← links)
- A proof outline logic for object-oriented programming (Q2571207) (← links)
- Dynamic inference of polymorphic lock types (Q2575137) (← links)
- Model checking, testing and verification working together (Q2576575) (← links)
- Are the logical foundations of verifying compiler prototypes matching user expectations? (Q2643125) (← links)
- Highly dependable concurrent programming using design for verification (Q2643127) (← links)
- Specification and verification challenges for sequential object-oriented programs (Q2643131) (← links)
- Faster and more complete extended static checking for the Java modeling language (Q2655328) (← links)
