JML - MaRDI portal

swMATH4597MaRDI QIDQ16768FDOQ16768

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

Snapshot Generation in a Constructive Object-Oriented Modeling Language
Executing formal specifications with concurrent constraint programming
Formal methods for smart cards: an experience report
Verification, Model Checking, and Abstract Interpretation
Verifying Whiley programs with Boogie
Building reliable, high-performance networks with the Nuprl proof development system
Formal verification of side-channel countermeasures using self-composition
A generic complete dynamic logic for reasoning about purity and effects
Specification and verification of invariants by exploiting layers in OO designs
Beyond contracts for concurrency
FM 2005: Formal Methods
Source code verification of a secure payment applet
Title not available (Why is that?)
Title not available (Why is that?)
Proof pearl: The KeY to correct and stable sorting
Verification conditions are code
A behavioral type system and its application in Ptolemy II
Synthesis of positive logic programs for checking a class of definitions with infinite quantification
Hardware-Dependent Proofs of Numerical Programs
Are the logical foundations of verifying compiler prototypes matching user expectations?
Observational purity and encapsulation
How the design of JML accommodates both runtime assertion checking and formal verification
Gray-box monitoring of hyperproperties with an application to privacy
Information flow in object-oriented software
Title not available (Why is that?)
A verifying compiler for a multi-threaded object-oriented language
A tool-supported proof system for multithreaded Java.
Theorem Proving in Higher Order Logics
Understanding parameters of deductive verification: an empirical investigation of KeY
Traits: correctness-by-construction for free
Title not available (Why is that?)
Unifying separation logic and region logic to allow interoperability
Programming Languages and Systems
Title not available (Why is that?)
Title not available (Why is that?)
A formal approach to adaptive software: continuous assurance of non-functional requirements
Integration of verification methods for program systems
A relational shape abstract domain
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
A case study in class library verification: Java's vector class
Theory and methodology of assumption/commitment based system interface specification and architectural contracts
Title not available (Why is that?)
Denotational semantics for a program logic of objects
The safety-critical Java memory model formalised
A logic of reachable patterns in linked data-structures
Compositionality for quantitative specifications
Fundamental Approaches to Software Engineering
Integrated approach to analysis and verification of imperative programs
Proving Theorems About JML Classes
A Hoare Logic for Call-by-Value Functional Programs
Proving the correctness of mobile Java code
Tools and Algorithms for the Construction and Analysis of Systems
A Realizability Model for Impredicative Hoare Type Theory
Class invariants as abstract interpretation of trace semantics
Algebraic Methodology and Software Technology
The Daikon system for dynamic detection of likely invariants
Title not available (Why is that?)
Method redefinition-ensuring alternative behaviors
Programming Languages and Systems
Tools and Algorithms for the Construction and Analysis of Systems
Tools and Algorithms for the Construction and Analysis of Systems
Featherweight Jigsaw. Replacing inheritance by composition in Java-like languages
Algebraic Methodology and Software Technology
Automata-based verification of programs with tree updates
Predicate abstraction in a program logic calculus
Contract-based verification of MATLAB-style matrix programs
Viper: a verification infrastructure for permission-based reasoning
On refinements of Boolean and parametric modal transition systems
An observationally complete program logic for imperative higher-order functions
Stepwise Development of Simulink Models Using the Refinement Calculus Framework
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
Assertion-based slicing and slice graphs
Coalgebras and monads in the semantics of Java
A program logic for resources
Verification of object-oriented programs: a transformational approach
A Representation-Independent Behavioral Semantics for Object-Oriented Components
FM 2005: Formal Methods
POSIX file store in Z/Eves: An experiment in the verified software repository
Refinement checking on parametric modal transition systems
Lazy behavioral subtyping
Debugging Maude programs via runtime assertion checking and trace slicing
Modular inference of subprogram contracts for safety checking
A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
Extending Model Checking with Dynamic Analysis
Title not available (Why is that?)
A shared-variable concurrency analysis of multi-threaded object-oriented programs
Modular specification and verification of object-oriented programs
A type safe state abstraction for coordination in JAVA-like languages
Title not available (Why is that?)
A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs
Verification conditions for source-level imperative programs
A dynamic logic for deductive verification of multi-threaded programs
Title not available (Why is that?)
Integrating a formal method into a software engineering process with UML and Java
Algebraic Methodology and Software Technology
Specification and runtime verification of Java card programs
JCML: A specification language for the runtime verification of Java card programs
Abstract Certification of Global Non-interference in Rewriting Logic

This page was built for software: JML