Cited in
(only showing first 100 items - show all)- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
- Executing formal specifications with concurrent constraint programming
- Class invariants as abstract interpretation of trace semantics
- Snapshot Generation in a Constructive Object-Oriented Modeling Language
- Tools and Algorithms for the Construction and Analysis of Systems
- Formal methods for smart cards: an experience report
- Second-Order Principles in Specification Languages for Object-Oriented Programs
- WP semantics and behavioral subtyping
- A Realizability Model for Impredicative Hoare Type Theory
- Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services
- Algebraic Methodology and Software Technology
- Verifying Whiley programs with Boogie
- Verification, Model Checking, and Abstract Interpretation
- Method redefinition-ensuring alternative behaviors
- The Daikon system for dynamic detection of likely invariants
- Skill-based verification of cyber-physical systems
- scientific article; zbMATH DE number 2090132 (Why is no real title available?)
- Model checking merged program traces
- Tools and Algorithms for the Construction and Analysis of Systems
- Formal verification of side-channel countermeasures using self-composition
- Programming Languages and Systems
- Building reliable, high-performance networks with the Nuprl proof development system
- A generic complete dynamic logic for reasoning about purity and effects
- scientific article; zbMATH DE number 1956485 (Why is no real title available?)
- Defining contracts with different tools in software development
- Specification and verification of invariants by exploiting layers in OO designs
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- Featherweight Jigsaw. Replacing inheritance by composition in Java-like languages
- Formalizing a hierarchical file system
- Automata-based verification of programs with tree updates
- Beyond contracts for concurrency
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification rules for exception handling in Eiffel
- Contract-based verification of MATLAB-style matrix programs
- Predicate abstraction in a program logic calculus
- Source code verification of a secure payment applet
- Tools and Algorithms for the Construction and Analysis of Systems
- Algebraic Methodology and Software Technology
- FM 2005: Formal Methods
- Proof pearl: The KeY to correct and stable sorting
- scientific article; zbMATH DE number 1617288 (Why is no real title available?)
- Algebraic Methodology and Software Technology
- scientific article; zbMATH DE number 2090026 (Why is no real title available?)
- Verification conditions are code
- Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
- A behavioral type system and its application in Ptolemy II
- A Bytecode Logic for JML and Types
- An observationally complete program logic for imperative higher-order functions
- Formalizing a hierarchical file system
- Verification of distributed systems with local-global predicates
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Viper: a verification infrastructure for permission-based reasoning
- On refinements of Boolean and parametric modal transition systems
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Stepwise Development of Simulink Models Using the Refinement Calculus Framework
- Assertion-based slicing and slice graphs
- Coalgebras and monads in the semantics of Java
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- A program logic for resources
- Verification of object-oriented programs: a transformational approach
- A Representation-Independent Behavioral Semantics for Object-Oriented Components
- Hardware-Dependent Proofs of Numerical Programs
- Access permission contracts for scripting languages
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- POSIX file store in Z/Eves: An experiment in the verified software repository
- Lazy behavioral subtyping
- Observational purity and encapsulation
- Debugging Maude programs via runtime assertion checking and trace slicing
- Modular inference of subprogram contracts for safety checking
- FM 2005: Formal Methods
- Refinement checking on parametric modal transition systems
- Decision based examination of object-oritented methodology using JML
- How the design of JML accommodates both runtime assertion checking and formal verification
- Gray-box monitoring of hyperproperties with an application to privacy
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- scientific article; zbMATH DE number 1953020 (Why is no real title available?)
- A shared-variable concurrency analysis of multi-threaded object-oriented programs
- Dafny
- HasCasl
- JMLUnit
- scientific article; zbMATH DE number 1693527 (Why is no real title available?)
- Modula
- Valigator
- WSAT
- POOC
- jContractor
- Virginity
- Symstra
- Ada95
- ArcAngel
- JavaFAN
- LARCH
- AGVI
- SCOOP
- ECDAR
- TASC
- KRAKATOA
- CLOS
- SPARK
- Eiffel
This page was built for software: JML
