JML

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
• Title not available (Why is that?)
• 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
• Information Flow in Object-Oriented Software
• Fundamental Approaches to Software Engineering
• Proving Theorems About JML Classes
• A Hoare Logic for Call-by-Value Functional Programs
• Proving the correctness of mobile Java code
• Second-Order Principles in Specification Languages for Object-Oriented Programs
• WP semantics and behavioral subtyping
• Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• Separation Logic Contracts for a Java-Like Language with Fork/Join
• Defining contracts with different tools in software development
• Verification rules for exception handling in Eiffel
• Algebraic Methodology and Software Technology
• A Bytecode Logic for JML and Types
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• Access permission contracts for scripting languages
• Decision based examination of object-oritented methodology using JML
• Title not available (Why is that?)
• ZB 2005: Formal Specification and Development in Z and B
• FM 2005: Formal Methods
• Model-Driven Monitoring: An Application of Graph Transformation for Design by Contract
• Skill-Based Verification of Cyber-Physical Systems
• Model Checking Merged Program Traces
• Formalizing a Hierarchical File System
• Principled Software Development
• Verification of Java Programs with Generics
• Truncation for Low-Complexity MIMO Signal Detection
• A refinement methodology for object-oriented programs
• Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
• 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
• Specification and Runtime Verification of Java Card Programs
• 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

This page was built for software: JML