JML

swMATH4597MaRDI QIDQ16768FDOQ16768

Author name not available (Why is that?)

Official website: http://www.eecs.ucf.edu/~leavens/JML/

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

• Snapshot Generation in a Constructive Object-Oriented Modeling Language
• Tools and Algorithms for the Construction and Analysis of Systems
• Executing formal specifications with concurrent constraint programming
• Class invariants as abstract interpretation of trace semantics
• Algebraic Methodology and Software Technology
• Formal methods for smart cards: an experience report
• Verification, Model Checking, and Abstract Interpretation
• Verifying Whiley programs with Boogie
• Title not available (Why is that?)
• Method redefinition-ensuring alternative behaviors
• Building reliable, high-performance networks with the Nuprl proof development system
• A generic complete dynamic logic for reasoning about purity and effects
• Specification and verification of invariants by exploiting layers in OO designs
• Automata-based verification of programs with tree updates
• 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
• Viper: a verification infrastructure for permission-based reasoning
• On refinements of Boolean and parametric modal transition systems
• Stepwise Development of Simulink Models Using the Refinement Calculus Framework
• Assertion-based slicing and slice graphs
• A program logic for resources
• A Representation-Independent Behavioral Semantics for Object-Oriented Components
• Hardware-Dependent Proofs of Numerical Programs
• FM 2005: Formal Methods
• Refinement checking on parametric modal transition systems
• SafeJML
• Observational purity and encapsulation
• Debugging Maude programs via runtime assertion checking and trace slicing
• How the design of JML accommodates both runtime assertion checking and formal verification
• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
• A shared-variable concurrency analysis of multi-threaded object-oriented programs
• Information flow in object-oriented software
• 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
• Title not available (Why is that?)
• Unifying separation logic and region logic to allow interoperability
• A deductive proof system for multithreaded Java with exceptions
• 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
• A case study in class library verification: Java's vector class
• Title not available (Why is that?)
• 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
• Compositionality for quantitative specifications
• Fundamental Approaches to Software Engineering
• Abstract Predicates and Mutable ADTs in Hoare Type Theory
• Proving Theorems About JML Classes
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• A Hoare Logic for Call-by-Value Functional Programs
• Code-carrying theories
• A Realizability Model for Impredicative Hoare Type Theory
• The Daikon system for dynamic detection of likely invariants
• 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
• Predicate abstraction in a program logic calculus
• Contract-based verification of MATLAB-style matrix programs
• 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
• Coalgebras and monads in the semantics of Java
• Verification of object-oriented programs: a transformational approach
• POSIX file store in Z/Eves: An experiment in the verified software repository
• Lazy behavioral subtyping
• Modular inference of subprogram contracts for safety checking
• Extending Model Checking with Dynamic Analysis
• Title not available (Why is that?)
• 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?)
• Ada95
• ACSL
• Caduceus
• JACK
• Frama-C
• Omnibus
• Valgrind
• Why3
• Spec#
• 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?)

This page was built for software: JML