The following pages link to JML (Q16768):
Displaying 50 items.
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- An observationally complete program logic for imperative higher-order functions (Q387994) (← links)
- Featherweight Jigsaw. Replacing inheritance by composition in Java-like languages (Q418193) (← links)
- Verification of distributed systems with local-global predicates (Q432134) (← links)
- Formalizing a hierarchical file system (Q432156) (← links)
- JCML: A specification language for the runtime verification of Java card programs (Q436381) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- Verification of object-oriented programs: a transformational approach (Q439944) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- A dynamic logic for deductive verification of multi-threaded programs (Q470007) (← links)
- Monitoring and recovery for web service applications (Q488218) (← links)
- Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers (Q497870) (← links)
- Predicate abstraction in a program logic calculus (Q549686) (← links)
- Incremental reasoning with lazy behavioral subtyping for multiple inheritance (Q549694) (← links)
- Modular inference of subprogram contracts for safety checking (Q604392) (← links)
- Lazy behavioral subtyping (Q710675) (← links)
- Verifying traits: an incremental proof system for fine-grained reuse (Q736803) (← links)
- Debugging Maude programs via runtime assertion checking and trace slicing (Q739630) (← links)
- jContractor: Introducing design-by-contract to Java using reflective bytecode instrumentation (Q812054) (← links)
- Method redefinition-ensuring alternative behaviors (Q834963) (← links)
- Automata-based verification of programs with tree updates (Q845236) (← links)
- Beyond contracts for concurrency (Q846113) (← links)
- Verification conditions are code (Q855274) (← links)
- Observational purity and encapsulation (Q882452) (← links)
- CPBPV: a constraint-programming framework for bounded program verification (Q968353) (← links)
- A generic complete dynamic logic for reasoning about purity and effects (Q973056) (← links)
- A shared-variable concurrency analysis of multi-threaded object-oriented programs (Q1004057) (← links)
- POSIX file store in Z/Eves: An experiment in the verified software repository (Q1004296) (← links)
- A type safe state abstraction for coordination in JAVA-like languages (Q1006341) (← links)
- Invariant based programming: Basic approach and teaching experiences (Q1019025) (← links)
- Integration of verification methods for program systems (Q1040327) (← links)
- Theory and methodology of assumption/commitment based system interface specification and architectural contracts (Q1654563) (← links)
- Class invariants as abstract interpretation of trace semantics (Q1749225) (← links)
- An assertion-based proof system for multithreaded Java (Q1770359) (← 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)
- Understanding parameters of deductive verification: an empirical investigation of KeY (Q1791175) (← links)
- Compositionality for quantitative specifications (Q1797783) (← links)
- Unifying separation logic and region logic to allow interoperability (Q1798668) (← links)
- Coalgebras and monads in the semantics of Java (Q1853752) (← links)
- Executing formal specifications with concurrent constraint programming (Q1857312) (← links)
- Weakest pre-condition reasoning for Java programs with JML annotations (Q1881666) (← links)
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML (Q1881670) (← links)
- Source code verification of a secure payment applet (Q1881671) (← links)
- A behavioral type system and its application in Ptolemy II (Q1882802) (← links)
- A formal approach to adaptive software: continuous assurance of non-functional requirements (Q1941849) (← links)
- Assertion-based slicing and slice graphs (Q1941855) (← links)
- The safety-critical Java memory model formalised (Q1941888) (← links)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
- A relational shape abstract domain (Q2058389) (← links)
