yusuke1997/dblp-id-title huggingface dataset:
A Formal Axiomatization for Alphabet Reasoning with Parametrized Processes
Local Invariance
In praise of algebra
TOrPEDO: witnessing model correctness with topological proofs
Review on Modelling and Verification of Secure Exams : By Rosario Giustolisi Springer, Cham, 2018, X, 133 pp, ISBN: 9783319671062 (Hardback, £89.99), ISBN: 9783030097899 (Paperback, £64.99), ISBN: 9783319671079 (eBook, £51.99)
Interfaces for Refining Recursion and Procedures
Data refinement and singleton failures refinement are not equivalent
Branching versus Linear Logics Yet Again
Eliminating the Substitution Axiom from UNITY Logic
A Minimal Graphical User Interface for the Jape Proof Calculator
From MC/DC to RC/DC: formalization and analysis of control-flow testing criteria
Accelerating worst case execution time analysis of timed automata models with cyclic behaviour
A computer checked algebraic verification of a distributed summation algorithm
Invariant based programming: basic approach and teaching experiences
Structural Refinement of Systems Specified in Object-Z and CSP
Building program construction and verification tools from algebraic principles
The List Introduction Strategy for the Derivation of Logic Programs
Compositional Failure-based Semantics Models for Basic LOTOS
From StPowla processes to SRML models
DUALITY: A Simple Formalism for the Analysis of UNITY
Ready for testing: ensuring conformance to industrial standards through formal verification
Class Refinement as Semantics of Correct Object Substitutability
Algebra and logic for access control
Concolic testing of the multi-sector read operation for flash storage platform software
Formal Performance Modelling and Evaluation of an Adaptive Mechanism for Packetised Audio over the Internet
Predicate Transformers for Recursive Procedures with Local Variables
Verification and falsification of programs with loops using predicate abstraction
An Approach to Literate and Structured Formal Developments
Compositional Verification of Real-Time Systems with Explicit Clock Temporal Logic
Assumption propagation through annotated programs
Generalised Stream X-Machines and Cooperating Distributed Grammar Systems
A framework for Satisfiability Modulo Theories
Michael J.C. Gordon FRS Professor of Computer Assisted Reasoning (28 February 1948-22 August 2017)
Redesign of a Systems Engineering Language: Formalisation of X
A refinement-based process algebra for timed automata
An approximation algorithm for state minimization in 2-MDFAs
Modelling and Validation: AUTOFOCUS and Quest
A formal approach for the construction and verification of railway control systems
A Case in Point: Verification and Testing of a EULYNX Interface
Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol
The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract
Concurrency and Refinement in the Unified Modeling Language
Introduction to the Special Collection from PRDC 2023
A Methodology for Designing Proof Rules for Fair Parallel Programs
Generalised folds for nested datatypes
Inter-process buffers in separation logic with rely-guarantee
Institution Morphisms
A general framework for architecture composability
Object-Extending Class Transformations
Overtaking in Asynchronous Periodic Systems
Model-driven synthesis of formally precise, stylized software architectures
Should ML be Object-Oriented?
Validating a web service security abstraction by typing
Benchmarking Combinations of Learning and Testing Algorithms for Automata Learning
From a domain analysis to the specification and detection of code and design smells
Specification and Correctness Proof of a WAM Extension with Abstract Type Constraints
A Collection of Papers and Memoirs Celebrating the Contribution of Rod Burstall to Advances in Computer Science
Automated Generation of Modular Assurance Cases with the System Assurance Reference Model
An integrated framework for the performance analysis of asynchronous communicating stochastic processes
Partial evaluation of string obfuscations for Java malware detection
Revising Z: Part II - Logical Development
Testing a deterministic implementation against a non-controllable non-deterministic stream X-machine
Formalising concurrent UML state machines using coloured Petri nets
A Formal Definition of Time in LOTOS
An Implementation of Syntax Directed Functional Programming on Nested-Stack Machines
On Simulation, Subtyping and Substitutability in Sequential Object Systems
A Logic for Schema-Based Program Development
Modeling and enhancement of the IEEE 802.11 RTS/CTS scheme in an error-prone channel
Using schedulers to test probabilistic distributed systems
Formal verification and quantitative metrics of MPSoC data dynamics
A formalisation of deep metamodelling
A denotational semantics for Handel-C
Procedure compilation in the refinement calculus
A Case Study in the Specification and Analysis of Design Alternatives for a User Interface
Component-wise incremental LTL model checking
Generic Composition
Invariant-based reasoning about parameterized security protocols
Assuring property conformance of code generators via model checking
Processes with Probablities, Priority and Time
The Co-invariant Generator: An Aid in Deriving Loop Bodies
Correctness and concurrent complexity of the Black-White Bakery Algorithm
Deciding Bisimilarity is P-Complete
Provably correct derivation of algorithms using FermaT
Streamlining progress-based derivations of concurrent programs
Specification and analysis of synchronous reactions
Denotational semantics of channel mobility in UTP-CSP
Not necessarily closed convex polyhedra and the double description method
Relational concurrent refinement part III: traces, partial relations and automata
Using probabilistic model checking for dynamic power management
Alternative shaper: a model for automatic design generation
Physigrams: modelling devices for natural interaction
Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
The Ancient Theory of Mind
Beyond contracts for concurrency
Adaptive distinguishing test cases of nondeterministic finite state machines: test case derivation and length estimation
Collaborative models for autonomous systems controller synthesis
Derivation of concurrent programs by stepwise scheduling of Event-B models
Formal modelling and verification of GALS systems using GRL and CADP
A New Approach to Abstract Syntax with Variable Binding
Stepwise refinement of heap-manipulating code in Chalice
L <Omega> UI : L ovely <Omega>MEGA U ser I nterface
A probability perspective
Denotational Semantics of an Object-Oriented Programming Language with Explicit Wrappers
Architectural refinement and notions of intransitive noninterference
VDM semantics of programming languages: combinators and monads
Towards verification of computation orchestration
Quantified abstract configurations of distributed systems
Verification of Mondex electronic purses with KIV: from transactions to a security protocol
Proof Movie - A Proof with the Boyer-Moore Prover
Automated circular assume-guarantee reasoning
A Single Complete Rule for Data Refinement
On termination and invariance for faulty channel machines
Synthesizing bounded-time 2-phase fault recovery
Denotational semantics and its algebraic derivation for an event-driven system-level language
Specifying the Apple Macintosh Toolbox Event Manager
SDLV: Verification of Steering Angle Safety for Self-Driving Cars
Automatic verification of reduction techniques in Higher Order Logic
A calculus of trustworthy ad hoc networks
Cameo: an alternative model of concurrency for Eiffel
A Method for Showing Progress
RoboWorld: Verification of Robotic Systems with Environment in the Loop
Specification, Verification and Prototyping of an Optimized Compiler
Security analysis of efficient (Un-)fair non-repudiation protocols
Abstract conjunctive partial deduction for the analysis and compilation of coroutines
Elucidating concurrent algorithms via layers of abstraction and reification
Testing Conditions for Communicating Stream X-machine Systems
A Tactic Calculus-Abridged Version
A Compositional Simulation Framework for Abstract State Machine Models of Discrete Event Systems
A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
The Sliding-Window Protocol Revisited
Translating FSP into LOTOS and networks of automata
Quantitative verification of Kalman filters
Testing Conformance to a Quasi-Non-Deterministic Stream X-Machine
Gerard O'Regan: Concise Guide to Formal Methods: Theory, Fundamentals and Industry Applications
Unification of Four Versions of Program Semantics
Deep Semantic Links of TCSP and Object-Z: TCOZ Approach
On Sequential Compoisiton, Action Prefixes and Process Prefixes
Minimal refinements of specifications in model and termporal logics
A singleton failures semantics for Communicating Sequential Processes
A formal relationship between program slicing and partial evaluation
Simple linear string constraints
Towards a Formal Treatment of Implicit Invocation Using Rely/Guarantee Reasoning
Tobias Nipkow and Gerwin Klein: Concrete Semantics with Isabelle/HOL - Springer Verlag, 2014, x + 289 pp, € 63, 29 (Hardback), ISBN 978-3-319-10542-0, http: //www.concrete-semantics.org/
Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds): Handbook of model checking - Springer International Publishing AG, Cham, Switzerland, 2018
Contracts for concurrency
Proving linearizability with temporal logic
Language and tool support for event refinement structures in Event-B
Modeling and Verification of Natural Language Requirements based on States and Modes
Model-based Safety Assessment of a Triple Modular Generator with xSAP
Towards a Formal Foundation of the Specification and Description Language SDL
Introduction to the Special Collection from FASE 2021
Symbolic execution formally explained
The Development and Deployment of Formal Methods in the UK
Formalising a Value-Passing Calculus in HOL
A Note on Kobayashi's and Yonezawa's "Asynchronous Communication Model Based on Linear Logic"
Formal Verification of a Railway Interlocking System using Model Checking
Estimating costs of multi-component enterprise applications
Emergence and refinement
Analysing sanity of requirements for avionics systems
An elementary and unified approach to program correctness
A fully verified container library
Defining, Analysing and Implementing Communication Protocols Using Attribute Grammars
Automatizing Parametric Reasoning on Distributed Concurrent Systems
Investigating the Integration of two Formal Methods
Statechartable Petri nets
Shallow Linear Action Graphs and their Embeddings
Verified Compilation of Communicating Processes into Clocked Circuits
An algebraic semantics for MOF
Exploiting augmented intelligence in the modeling of safety-critical autonomous systems
An Overview of the Integrated Formalism RT-Z
Compositional Reasoning for Non-multicopy Atomic Architectures
Conditional Composition
Formal probabilistic analysis of detection properties in wireless sensor networks
Model checking with bounded context switching
Abstract Data Types Can Have Inequations1
Experiments in program verification using Event-B
Event-based run-time adaptation in communication-centric systems
An Event-B based approach for cloud composite services verification
Bisimulation and Coinduction Enhancements: A Historical Perspective
Dependently Typed Records in Type Theory
On the Lattice of Specifications: Applications to a Specification Methodology
Meta-interpreters and Partial Evaluation in Parlog
Data Refinement of Remote Procedures
A unified integration and component testing approach from deterministic stream X-machine specifications
Model-checking timed automata with deadlines with Uppaal
A secure voting scheme based on rational self-interest
Coquand's Calculus of Constructions: A Mathematical Foundation for a Proof Development System
A modeling and verification framework for optical quantum circuits
The Tree Identify Protocol of IEEE 1394 in µCRL
Reo + mCRL2: A framework for model-checking dataflow in service compositions
Are the Logical Foundations of Verifying Compiler Prototypes Matching user Expectations?
Designing a semantic model for a wide-spectrum language with concurrency
Starvation-free mutual exclusion with semaphores
On building cyclic and shared structures in Haskell
On theorem prover-based testing
Specifying Distributed CICS in Z: Accessing Local and Remote Resources (Short Communication)
A process calculus BigrTiMo of mobile systems and its formal semantics
Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs
Specification and Verification of the Tree Identify Protocol of IEEE 1394 in Rewriting Logic
Unification: A Case-Study in Data Refinement
ASM-based formal design of an adaptivity component for a Cloud system
Review on : Domain Science and Engineering - A Foundation for Software Development: By Dines Bjørner Monographs in Theoretical Computer Science, Springer International Publishing, ISBN 3030734831, 1st ed., 400 pages, 2021
Interactive tool support for CSP || B consistency checking
A Program Refinement Tool
Relational Concurrent Refinement
Contract-based verification of MATLAB-style matrix programs
Deriving Proof Rules from Continuation Semantics
Generalised multi-pattern-based verification of programs with linear linked structures
Theoretical and Practical Approaches to the Denotational Semantics for MDESL based on UTP
The Standard Logic of Z is Inconsistent
Probabilistic may/must testing: retaining probabilities by restricted schedulers
Testing Algebraic Data Types and Processes: A Unifying Theory
Introduction to the Special Section on FM 2021
A Logical Framework for Evolving Software Systems
Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL
A practical comparison of Alloy and Spin
Strategy based semantics for mobility with time and access permissions
ZRC - A Refinement Calculus for Z
Footprint Logic for Object-Oriented Components (extended paper)
An explicit transition system construction approach to LTL satisfiability checking
GR(1)*: GR(1) specifications extended with existential guarantees
An assertional proof for a construction of an atomic variable
Mechanising Mondex with Z/Eves
Enhancing Robustness Verification for Deep Neural Networks via Symbolic Propagation
Design for Proof: An Approach to the Design of Domain-Specific Languages
Towards a linear algebra of programming
The Concept of Class Invariant in Object-oriented Programming
Dijkstra, Floyd and Warshall meet Kleene
Combining Component Specifications in Object-Z and CSP
Filter-embedding semiring fusion for programming with MapReduce
Model-checking user behaviour using interacting components
From Non-punctuality to Non-adjacency: A Quest for Decidability of Timed Temporal Logics with Quantifiers
Formally sound implementations of security protocols with JavaSPI
A lazy approach to symmetry reduction
Exploring Scalability of BFT Blockchain Protocols through Network Simulations
Generalised Stream X-Machines with Output Delimited Type
Properties of Concurrent Programs
André Platzer: Logical foundations of cyber-physical systems
Interactive verification of architectural design patterns in FACTum
Program Morphisms
The Weakest Precondition Calculus: Recursion and Duality
A Logic for Miranda, Revisited
The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs
Bernhard Steffen, Oliver R¨uthing, and Michael Huth: Mathematical Foundations of Advanced Informatics - Volume 1: Inductive Approaches - Springer, 2 April 2018, 258 pp, 156x16x234mm, ISBN-13: 978-3319683966 (Hardback, £28.99), ISBN: 978-3030098339 (Paperback, £27.99)
Some Facile Chemistry
Refinement-Oriented Probability for CSP
Transforming Boolean equalities into constraints
Algebra-Based Reasoning for Loop Synthesis
Formal Methods in Industry
A Mechanically Verified Incremental Garbage Collector
Formalizing non-interference for a simple bytecode language in Coq
Network invariants for real-time systems
Partial Order Behaviour and Structure of Petri Nets
Responsiveness and stable revivals
On proving confluence modulo equivalence for Constraint Handling Rules
Progress Assumption in Concurrent Systems
Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation
A tableau-based decision procedure for CTL
The Applicability of Discrete Performance Estimation Methods to VLSI Design
Checking noninterference in Timed CSP
A Strict Functional Language with Cyclic Recursive Data
Issues in the Design of a Parallel Object-Oriented Language
Tests and proofs for custom data generators
Model-based testing of probabilistic systems
Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker
A functional formalization of on chip communications
Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-B
Presheaves as Configured Specifications
Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
A formal approach to adaptive software: continuous assurance of non-functional requirements
Three tokens in Herman's algorithm
On Closure Under Stuttering
Synthesizing and verifying controllers for multi-lane traffic maneuvers
An engineering process for the verification of real-time systems
A Model Checker for Linear Time Temporal Logic
Model checking, testing and verification working together
Superposition Refinement of Reactive Systems
A Nitpick Analysis of Mobile IPv6
Equivalence of Formal Semantics Definition Methods
Automated mutual induction proof in separation logic
A refinement-based development of a distributed signalling system
A Refinement Calculus for Specifications in Hennessy-Milner Logic with Recursion
A Formal Model of Explanation
Exits in the Refinement Calculus
Formal relational database design: an exercise in extending the formal template language
Type Interference in Stack Based Languages
Runtime enforcement of timed properties using games
Manifest domains: analysis and description
Review of Formal Methods: An Appetizer : By Flemming Nielson and Hanne Riis Nielson Springer, 2019, ISBN 978-3-030-05155-6, https: //link.springer.com/book/10.1007/978-3-030-05156-3, pp. 1-160
Exploring Tabular Verification and Refinement
On the Interactive Power of Higher-order Processes Extended with Parameterization
Semantic inheritance in unifying theories of programming
Deciding probabilistic automata weak bisimulation: theory and practice
Partiality and Nondeterminacy in Program Proofs
A Static View of Localities
Hoare Logic and Auxiliary Variables
External and internal choice with event groups in Event-B
A behavioral type system and its application in Ptolemy II
Edsger Wybe Dijkstra (1930-2002): A Portrait of a Genius
Formalizing and testing the consistency of DSL transformations
Integrating stochastic reasoning into Event-B development
On dual programs in co-logic programming and the Horn μ -calculus
A formal framework for service modeling and prototyping
The Semantics of the Combination of Atomized Statements and Parallel Choice
Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems
Introduction to the Special Collection from the International Conference on Tests and Proofs (TAP) 2020 and 2021
Model checking CML: tool development and industrial applications
Invariants and Closures in the Theory of Rewrite Systems
Structured Development of a Virtual Shared Memory System
Modelling and Verifying of a 'Cash-Point Service' Using MOBY/PLC
Model checking action system refinements
An inductive characterization of matching in binding bigraphs
Intensional and Extensional Semantics of Dataflow Programs
Analysing an autonomous tramway positioning system with the Uppaal Statistical Model Checker
Partial Logics Reconsidered: A Conservative Approach
Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing
Almost ASAP semantics: from timed models to timed implementations
Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESL
Computation tree measurement language (CTML)
Interpreting Message Flow Graphs
An algebraic approach to the design of compilers for object-oriented languages
Computing Permutation Encodings
Enhancing Probabilistic Model Checking with Ontologies
Generalised rely-guarantee concurrency: an algebraic foundation
Term Rewriting and Beyond - Theorem Proving in Isabelle
A Multi-formalism Approach for the Validation of UML Models
Testing methods for X-machines: a review
Test generation from state based use case models
Kaisa Sere: In Memoriam
Invariant diagrams with data refinement
Milestones from the Pure Lisp theorem prover to ACL2
Structured Calculational Proof
A Deep Reinforcement Learning Framework with Formal Verification
Model checking dynamic pushdown networks
How to Write a Long Formula (Short Communication)
Capture-avoiding substitution as a nominal algebra
Automated property verification for large scale B models with ProB
An Introduction to Real-Time Object-Z
Probabilistic Duration Calculus for Continuous Time
Formal analysis of the compact position reporting algorithm
Sound Runtime Assertion Checking for Memory Properties via Program Transformation
CaPiTo: protocol stacks for services
A reduced maximality labeled transition system generation for recursive Petri nets
Parameterized Verification of Linear Networks using Automata as Invariants
Highly dependable concurrent programming using design for verification
Formalization of Camera Pose Estimation Algorithm based on Rodrigues Formula
Verifying anonymity in voting systems using CSP
A language-independent proof system for full program equivalence
Verification of distributed systems with the axiomatic system of MSVL
Verifying Programs in the Calculus of Inductive Constructions
Proof producing synthesis of arithmetic and cryptographic hardware
Introduction to the Special Collection from FM 2023
Flexible access control policy for SCOOP
Refining autonomous agents with declarative beliefs and desires
Model checking Duration Calculus: a practical approach
Architectural CCS
Reasoning About Exceptional Behavior At the Level of Java Bytecode with ByteBack
Sharp Retrenchment, Modulated Refinement and Simulation
Birkhoff style calculi for hybrid logics
Model checking Petri nets with names using data-centric dynamic systems
'The Standard Logic for Z': A Clarification
Essential Concepts of Algebraic Specification and Program Development
Actors and their Composition
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
Modelling and Verification of PREMO Synchronisable Objects
Modularising the Specification of a Small Database System in Extended ML
Cost vs. time in stochastic games and Markov automata
Partial-order Reduction Techniques for Real-time Model Checking
The mechanical generation of fault trees for reactive systems via retrenchment I: combinational circuits
Proving as Editing HOL Tactics
Verification of a sliding window protocol in µCRL and PVS
Modelling timed reactive systems from natural-language requirements
Tank monitoring: a pAMN case study
A mini challenge: build a verifiable filesystem
Refinement patterns for ASTDs
A Debugging Game for Probabilistic Models
Model checking learning agent systems using Promela with embedded C code and abstraction
A Comparison of Simulation Techniques and Algebraic Tachniques for Verifying Concurrent Systems
The Least Conjunctive Refinement and Promotion in the Refinement Calculus
Review on Functional Algorithms, Verified! : By Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan Freely downloadable: https://functional-algorithms-verified.org
A tale of two graph models: a case study in wireless sensor networks
A Logic for Miranda
Practice-oriented courses in formal methods using VDM ++
The Variety of Variables in Automated Real-Time Refinement
An SMT-Based Approach to the Verification of Knowledge-Based Programs
Preserving correctness during business process model configuration