yusuke1997/dblp-id-title huggingface dataset:
Proof by Analogy in Mural
Concurrent software verification with states, events, and deadlocks
The stream-based service-centred calculus: a foundation for service-oriented programming
Automating Event-B invariant proofs by rippling and proof patching
Specification and Refinement of Networks of Asynchronously Communicating Agents Using the Assumption/Commitment Paradigm
Broadcast MSCs
A Mechanical Proof of Segall's PIF Algorithm
Time-budgeting: a component based development methodology for real-time embedded systems
Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter
A CCS-based Investigation of Deadlock in a Multi-process Electronic Mail System
Deterministic concurrent strategies
Using a Formal Specification Contractually
The Changing Face of Standardization: A Place for Formal Methods?
The verified software repository: a step towards the verifying compiler
Demonstrating the Cognitive Plausibility of Interactive System Specifications
Winskel is (almost) Right: Towards a Mechanized Semantics
A comparison of tools for teaching formal software verification
Cut branches before looking for bugs: certifiably sound verification on relaxed slices
Program Algebra for Component Code
Modular Structuring of VDM Specifications in VVSL
Unifying separation logic and region logic to allow interoperability
Formal techniques for performance analysis: blending SAN and PEPA
Peter Landin: a computer scientist who inspired a generation, 5th June 1930 - 3rd June 2009
Polymorphic dynamic programming by algebraic shortcut fusion
A Principle for Sequential Reasoning about Distributed Algorithms
On Equivalence-Completions of Fairness Assumtions
Waitfree Linearization of an Arbitrary Data Object
Categorical ML - Category-Theoretic Modular Programming
Linearizability on hardware weak memory models
Real Time Process Algebra
A UTP approach for rTiMo
Constructing checking sequences for distributed testing
The data type of spatial objects
Proving termination of nonlinear command sequences
A Calculus and logic of resources and processes
Towards a Semantics-Based Information Theory
Correct Translation of Data Parallel Assignment onto Array Processors
Mutation Testing in the Refinement Calculus
Temporal-logic property preservation under Z refinement
A Dynamic Logic for deductive verification of multi-threaded programs
Explanatory Denotational Semantics for Complex Event Patterns
FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static Analysis
Thread algebra for strategic interleaving
An algebraic theory for web service contracts
Editorial: Where Theory and Practice Meet
Generating tests from B specifications and dynamic selection criteria
Program equivalence by circular reasoning
Rigorous development of component-based systems using component metadata and patterns
Algebraic Composition of Function Tables
Fast Automated Abstract Machine Repair Using Simultaneous Modifications and Refactoring
Formalization of Time and Space
An application of temporal projection to interleaving concurrency
Expressive Power of Specification Languages
Probabilistic verification of Herman's self-stabilisation algorithm
Thread algebra for poly-threading
An abstract model of service discovery and binding
The Universality of Functions in the Sciences at Large and in Computing
Provably-correct hardware compilation tools based on pass separation techniques
Proof Obligations for Blocks and Procedures
Responsiveness of interoperating components
EWD1300: The Notational Conventions I Adopted, and Why
Self-adaptation and secure information flow in multiparty communications
Verifying a Distributed List System: A Case History
iStar Goal Model to Z Formal Model Translation and Model Checking of CBTC Moving Block Interlocking System
Extending Hoare Logic to Real-Time
A verification and deployment approach for elastic component-based applications
Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
Symbolic predictive analysis for concurrent programs
Refinement of a Typed WAM Extension by Polymorphic Order-Sorted Types
Maximal incompleteness as obfuscation potency
Distributed Maximum Maintenance on Hierarchically Divided Graphs
Cryptographic protocols with everyday objects
Tight Error Analysis in Fixed-point Arithmetic
Using Event-B to construct instruction set architectures
Proofs-as-Programs as a Framework for the Design of an Analogy-Based ML Editor
Formal Aspects of Correctness and Optimality of Interval Computations
Special Collection on Computer Science Education
Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps
Encoding, Decoding and Data Refinement
Erratum to: Algebra and logic for access control
Computing maximal weak and other bisimulations
Drawing with SAT: four methods and A tool for producing railway infrastructure schematics
Specification and verification challenges for sequential object-oriented programs
Program Development in the Constructive Set Theory TK
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
The Systematic Construction of a One-Combinator Basis for Lambda-Terms
Safety, Liveness and Fairness in Temporal Logic
An elementary theory of product-line variations
Formal analysis of the kinematic Jacobian in screw theory
Sharing Analysis Based on Type Interface
Specifying and Refining Internal Operations in Z
Unifying theories in ProofPower-Z
A Security Flow Control Algorithm and Its Denotational Semantics Correctness Proof
Automated Analysis of Mutual Exclusion Algorithms using CCS
A Semantics for Distributed Execution of Statemate
The Fixed Point Theory of Unbounded Non-Determinism
Active learning for extended finite state machines
Compositional modeling of railway Virtual Coupling with Stochastic Activity Networks
Deciding orthogonal bisimulation
Algebraic Models of Correctness for Microprocessors
Relating trace refinement and linearizability
On Formal Methods Thinking in Computer Science Education
The Use of SI-Algebra in the Design of Sequencer Circuits
Categorical foundations for structured specifications in Z
Knaster-Tarski Revisited
UNITY and Büchi automata
Formal reliability analysis of redundancy architectures
Test-data generation for control coverage by proof
Functional Specification and Proof of Correctness for Time Dependent Behaviour of Reactive Systems
Formalizing a hierarchical file system
Angelic nondeterminism in the unifying theories of programming
Mechanised Safety Verification for a Distributed Autonomous Railway Control System
Deductive verification of alternating systems
Compositional Minimisation of Finite State Systems Using Interface Specifications
A formalism to describe design patterns based on role concepts
The certification of the Mondex electronic purse to ITSEC Level E6
Real space process algebra
A data-flow approach to test multi-agent ASMs
Testing interruptions in reactive systems
A Theory pf Orwellian Specifications with NewThink
Modeling and Verification of A Timing Protection Mechanism in the OSEK/VDX OS using CSP
An Algebraic Semantic Framework for Object Oriented Languages with Concurrency (Extended Abstract)
Towards formally specifying and verifying transactional memory
Refinement, Conformance and Inheritance
Model checking RAISE applicative specifications
Generating certified code from formal proofs: a case study in homological algebra
A programming model for BSP with partitioned synchronisation
Hybrid dynamic logic institutions for event/data-based systems
Retargeting a Hardware Compiler Using Protokol Converters
Cache Coherency in SCI: Specification and a Sketch of Correctness
Refinement-based verification of implementations of Stateflow charts
An Algebraic Characterisation of Elementary Net System (Observable) State Space
Security invariants in discrete transition systems
Completeness of a combination of neighbourhood logic and temporal logic
Comparing model checking and logical reasoning for real-time systems
Context Induction: A Proof Principle for Behavioural Abstractions and Algebraic Implementations
Refinement for user interface designs
Multiple model synchronization with multiary delta lenses with amendment and K-Putput
Zohar Manna (1939-2018)
Maximally Concurrent Programs
Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV
Representational Reasoning and Verification
Development Methods for Trusted Computer Systems
A formal approach for detection of security flaws in the android permission system
Bisimulations in calculi modelling membranes
JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-guided Fuzzing and Runtime Assertion Checking
On the expressive power of CSP refinement
Computable Processes and Bisimulation Equivalence
Inductive study of confidentiality: for everyone
Rooted Divergence-Preserving Branching Bisimilarity is a Congruence for Guarded CCS
On the limits of refinement-testing for model-checking CSP
A Reification Calculus for Model-Oriented Software Specification
Heterogeneous Notations for Pure Formal Method Integration
Validation of CHC Satisfiability with ATHENA
On partial state matching
Machine learning steered symbolic execution framework for complex software code
Weakest Preconditions for Progress
From LCF to Isabelle/HOL
Untanglings: a novel approach to analyzing concurrent systems
Verification of distributed systems with local-global predicates
The SH-Verification Tool - Abstraction-Based Verification of Co-operating Systems
Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM
Deriving non-Zeno behaviour models from goal models using ILP
The Completeness of Functional Logic
On assertion-based encapsulation for object invariants and simulations
BPPChecker: An SMT-based Model Checker on Basic Parallel Processes
The dynamic frames theory
On the Use of Data Refinement in the Development of Secure Communications Systems
The Connection Between Initial and Unique Solutions of Domain Equations in the Partial Order and Metric Approach
Empirical Architecture Comparison of Two-input Machine Learning Systems for Vision Tasks
Axioms and Models of Linear Logic
On the diversity of asynchronous communication
SMT based parameter identifiable combination detection for non-linear continuous and hybrid dynamics
Interval timed coloured Petri net: efficient construction of its state class space preserving linear properties
How to stop time stopping
Hoare's Logic and VDM
Normalising the Associative Law: An Experiment with Martin-Löf's Type Theory
Compositional Verification of Railway Interlocking Systems
Egon Börger and Alexander Raschke: Modeling companion for software practitioners - Springer, 2018, XXI+349 pp, ISBN: 978-3-662-56639-8 (Paperback, £ 46.99), eISBN: 978-3-662-56641-1 (eBook, £ 36.99), http: //dx.doi.org/10.1007/978-3-662-56641-1
Symbolic decision procedure for termination of linear programs
Introduction to the Special Collection from iFM 2022
Solutions of equations in languages
Process Simulation and Refinement
Verification of clock synchronization algorithms: experiments on a combination of deductive tools
Consistency-preserving refactoring of refinement structures in Event-B models
Verifying traits: an incremental proof system for fine-grained reuse
Mondex , an electronic purse: specification and refinement checks with the Alloy model-finding method
Predicate diagrams for the verification of real-time systems
A formal framework for modeling and validating Simulink diagrams
ω-Regular Energy Problems
Type Inference with Non-Structural Subtyping
Minimal refinements of specifications in modal and temporal logics
Interface synthesis and protocol conversion
A Fast Pattern Matching Algorithm Derived by Transformational and Assertional Reasoning
Formal verification of security protocol implementations: a survey
Discovering applications of higher order functions through proof planning
ADL: An Activity Description Language for Real-Time Networks
Battery-aware scheduling in low orbit: the GomX-3 case
Proof-based verification approaches for dynamic properties: application to the information system domain
How testing helps to diagnose proof failures
Finite Integer Computations: An Algebraic Foundation for Their Correctness
Simulation testing of automata
Toward automatic verification of quantum programs
Advanced Features of Duration Calculus and Their Applications in Sequential Hybrid Programs
The symbiosis of concurrency and verification: teaching and case studies
Online First Publication
An operational semantics for object-oriented concepts based on the class hierarchy
Editorial (VSTTE Special Issue)
A CSP model of Eiffel's SCOOP
Impact of Performance Considerations on Formal Specification Design
In Memoriam: Ernest Allen Emerson II
Verifying a signature architecture: a comparative case study
Using formal reasoning on a model of tasks for FreeRTOS
Reasoning about Dynamically Evolving Process Structures
Daniel Kroening and Ofer Strichman: Decision procedures - Springer Verlag, 2016, XXI, +356 ISBN 978-3-662-50496-3 (Hardback, €69, 67), http: //www.decision-procedures.org/
Correct-by-construction model driven engineering composition operators
A linear algebra approach to OLAP
Duration-constrained regular expressions
ProFeat: feature-oriented engineering for family-based probabilistic model checking
Generating invariants for non-linear loops by linear algebraic methods
On Verification of Parallel Message-Passing Processes
Foundations of programming languages
An Action-Based Formal Model for Concurrent Real-Time Systems
False Loop Detection in the IEEE 1394 Tree Identify Phase
Deriving dense linear algebra libraries
A formalization of geometric constraint systems and their decomposition
A generic complete dynamic logic for reasoning about purity and effects
Program verification with interacting analysis plugins
Modeling and analysis of communicating systems
Rod Burstall: In Memoriam
Generating Test Sets from Non-Deterministic Stream X-Machines
Counterexample-guided inductive synthesis for probabilistic systems
Complete deterministic stream X-machine testing
Mechanized proofs of opacity: a comparison of two techniques
Introduction to the Special Section on iFM 2020
Graph Transformation Units with Interleaving Semantics
Event Fairness and Non-interleaving Concurrency
An axiomatic approach to existence and liveness for differential equations
The First World Congress on Formal Methods in the Development of Computing Systems
Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism
Integration of UML and VHDL-AMS for analogue system modelling
A Refinement Strategy for Circus
State Machines for Large Scale Computer Software and Systems
Retrenchment for Event-B: UseCase-wise development and Rodin integration
Calculate Categorically!
Types with Intersection: An Introduction
Definition and Basic Properties of the Deva Meta-Calculus
Towards Formal Verification of a TPM Software Stack: Achievements and Opportunities
A Logic for Reasoning about Time and Reliability
Formal reliability and failure analysis of ethernet based communication networks in a smart grid substation
A program analysis framework for tccp based on abstract interpretation
Blaming the client: on data refinement in the presence of pointers
Using VDMTools to Model and Validate the Cash Dispenser Example
Mechanizing compositional reasoning for concurrent systems: some lessons
The specification logic nuZ
Refinement is complete for implementations
A process algebraic framework for specification and validation of real-time systems
Characterisations of testing preorders for a finite probabilistic π-calculus
Symbolic Approaches to Probability Distributions in Process Algebra
Specification by Interface Separation
Generation of complete test suites from mealy input/output transition systems
Special section of Tests and Proofs 2016
Obituary: Ole-Johan Dahl
Equality of Agent Expressions is preserved Under an Extension of the Universe of Actions
A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems
Compositional reasoning about active objects with shared futures
Atomic actions, and their refinements to isolated protocols
On integrating confidentiality and functionality in a formal method
Reasoning about orchestrations of web services using partial correctness
Theories for Mechanical Proofs of Imperative Programs
The NDB Database Specified in the RAISE Specification Language
John Warner Backus: 3 Dec 1924-17 March 2007
Integrating a formal method into a software engineering process with UML and Java
Obituary for Niklaus Wirth
Compositional Comparison of Formal Software Specifications Using Transformation Systems
TIC: A TImed Calculus
A compositional Petri net translation of general pi -calculus terms
The Consistency Theorem for Free Type Definitions in Z
Towards a Practitioners' Approach to Abadi and Lamport's Method
Stability, Sequentiality and Demand Driven Evaluation in Dataflow
John McCarthy (1927-2011)
An Algebraic Verification of a Mobile Network
Reconciling real and stochastic time: the need for probabilistic refinement
LOTOS Extended with Probablistic Behaviours
Amir Pnueli - A Gentle Giant: Lord of the phi 's and the psi 's
A Proof Sustem for Communicating Processes with Value-Passing
The Formalization of a Cognitive Architecture and its Application to Reasoning About Human Computer Interaction
Limits of Formal Methods
Foundations for using linear temporal logic in Event-B refinement
Explanation of two non-blocking shared-variable communication algorithms
Action Systemes, Unbounded Nondeterminism, and Infinite Traces
Event Refinement in State-Based Concurrent Systems
Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies
SCTL-MUS: A Formal Methodology for Software Development of Distributed Systems. A Case Study
Verification-guided modelling of salience and cognitive load
Ode to Rod Burstall
Refinement in hybridised institutions
Axiomatic Treatment of Processes with shared Variables Revisited
Introduction to the Special Section on Reliability, Safety, and Security of Railway Systems
The relation between preset distinguishing sequences and synchronizing sequences
A Hoare logic for linear systems
Analysis of a biphase mark protocol with Uppaaland PVS
A rigorous methodology for specification and verification of business processes
Automated verification and refinement for physical-layer protocols
A Functional Logic for Higher Level Reasoning About Computation
Model-Checking Discrete Duration Calculus
Design of an Automatic Teller Machine with Esterel Studio
Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
A Blocking Model for Reactive Objects
The behavioural semantics of Event-B refinement
Machine Checked Proofs of the Design of a Fault-Tolerance Circuit
Using refinement calculus techniques to prove linearizability
Information gain of black-box testing
The ASM Refinement Method
Proof Rules for Recursive Procedures
Analysing Cognitive Behaviour using LOTOS and Mexitl
Paramorphisms
The RISC ProofNavigator: a proving assistant for program verification in the classroom
Communicating Processes with Value-passing and Assignments
An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems
The Humble Humorous Researcher: A Tribute to Michel Sintzoff
Semantics of the probabilistic Lambda Calculus By Dirk Draheim
A Demonstrably Correct Compiler
Performance analysis of probabilistic action systems
Formal Methods Europe Update
Canonical Automata for Persistent Linearizability - A Corrigendum
Trace Semantics for C++11 Memory Model
Read atomic transactions with prevention of lost updates: ROLA and its formal analysis
Modeling and validating Mondex scenarios described in UML and OCL with USE
Specification of communicating processes: temporal logic versus refusals-based refinement
A Criterion for Atomicity
VDM and Z: A Comparative Case Study
Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus (FireWire) Protocol
Compositional refinement in agent-based security protocols
Assembling a prehistory for formal methods: a personal view
When is Partial Trace Equivalence Adequate?
Complete model-based equivalence class testing for nondeterministic systems
On the Interconnection Constants of Hopfield Nets
Transformations of Normal and Inverted Function Tables
Automatic Verification of a Lip-Synchronisation Protocol Using Uppaal
Integrating Predicate Transition Nets with First Order Temporal Logic in the Specification and Verification of Concurrent Systems
A semantics comparison workbench for a concurrent, asynchronous, distributed programming language
A framework for model transformation verification
Errata for Formal Aspects of Computing (2006) 18: 495-517 and their consequences
Specifying Cash-Point with DisCo
Revising Z: Part I - Logic and Semantics
Analysing neurobiological models using communicating automata
A Verification System for Current Programs Based on the Boyer-Moore Prover
Termination and Expressiveness of Execution Strategies for Networks of Bidirectional Model Transformations
Parametric probabilistic transition systems for system design and analysis
The Formalization and Analysis of a Communications Protocol
Social and Semiotic Analyses for Theorem Prover User Interface Design 1
Verification of EB 3 specifications using CADP
ArcAngel: a Tactic Language for Refinement
Review on Formal Methods for Software Engineering: Languages, Methods, Application Domains
Building a push-button RESOLVE verifier: Progress and challenges
Tool support for learning Büchi automata and linear temporal logic
Scalable context-dependent analysis of emergency egress models
Probabilistic Bigraphs
Assume-guarantee synthesis for digital contract signing
An analysis of refinement in an abortive paradigm
Introduction to the Special Collection from FACS 2022
From generic partition refinement to weighted tree automata minimization
Transformation of Programs for Fault-Tolerance
Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
Atomicity failure and the retrenchment atomicity pattern
Process algebraic modelling of attentional capture and human electrophysiology in interactive systems
Timed CCP compositionally embeds Argos and Lustre
A Survey of Practical Formal Methods for Security
Measurement-Noise Filtering for Automatic Discovery of Flow Splitting Ratios in ISP Networks
VVSL: A Language for Structured VDM Specifications
Structural transformations for data-enriched real-time systems
Verifying correctness of persistent concurrent data structures: a sound and complete method
Guest Editorial Integrated Formal Methods
Refinement algebra for probabilistic programs
Interactive Proof Critics
Dynamical Quantities in Net Systems
Verifying data refinements using a model checker
Error in the UNITY Rule for Subscripted Operators (Short Communication)
The formal design of distributed controllers with d SL and Spin
Balancing expressiveness in formal approaches to concurrency
Optimising the ProB model checker for B using partial order reduction
SecCT: Secure and Scalable Count Query Models on Encrypted Genomic Data
Integration of Parametric and "ad hoc" Second Order Polymorphism in a Calculus with Subtyping
Example Verifications Using Alphabet Axioms
Statistical model checking for variability-intensive systems: applications to bug detection and minimization
A Refinement-based Formal Development of Cyber-physical Railway Signalling Systems
But What if I Don't Want to Wait Forever?
Constraint logic programming with a relational machine
The 'Cash-Point' Service: A Verification Case Study Using STeP
Exploring probabilistic bisimulations, part I
Compensation by design
Proving completeness of logic programs with the cut
Reasoning about goal-directed real-time teleo-reactive programs
The Rest Says Unchanged (Concurrency and State-Based Specification)
Formalizing provable anonymity in Isabelle/HOL
Two Implementation Relations and the Correctness of Communicating Replicated Processes
Stepwise development and model checking of a distributed interlocking system using RAISE
Abstraction and approximation in fuzzy temporal logics and models