yusuke1997/dblp-id-title huggingface dataset:
Abstract Alloy Instances
Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned
Julienne: A Trace Slicer for Conditional Rewrite Theories
Encoding Fairness in a Synchronous Concurrent Program Algebra
Applications of Modal Logic for the Specification of Real-Time Systems
Security, Probability and Nearly Fair Coins in the Cryptographers' Café
Z/EVES Version 1.5: An Overview
Design of an Automatic Prover Dedicated to the Refinement of Database Applications
Interacting State Machines for Mobility
Analysis and Visualization of Performance Indicators in University Admission Tests
Mining Digital Twins of a VPN Server
A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures
Two Approaches towards the Formalisation of VDM
A Debugger for a Meta-IV-like Meta-Language
Compositional Binding in Network Domains
A Graph-Based Transformation Reduction to Reach UPPAAL States Faster
Proceedings of the Workshop on Applications of Formal Methods and Digital Twins co-located with 25th International Symposium on Formal Methods (FM 2023), Lübeck, Germany, March 06, 2023
On Formal Specification of a Proof Tool
Viewpoint Consistency in Z and LOTOS: A Case Study
Migrating the INTO-CPS Application to the Cloud
From Informal Requirements to COOP: A Concurrent Automata Approach
Java Applet Correctness: A Developer-Oriented Approach
Z Specification of an Object Manager
Combining Transformation and Posit-and Prove in a VDM Development
SCJ: Memory-Safety Checking without Annotations
Floating-Point Verification
Featured Team Automata
Formal Verification of Intelligent Hybrid Systems that are Modeled with Simulink and the Reinforcement Learning Toolbox
Towards OCL/RT
Scientific Decisions which Characterize VDM
A Systematic Approach to Transform OMT Diagrams to a B Specification
The VerCors Tool for Verification of Concurrent Programs
VDM as a Specification Method for Telecommunications Software
Specification-Based Test Repair Using a Lightweight Formal Method
The IBM Z Tool
Seven More Myths of Formal Methods
Graphical Specification and Reasoning: Case Study Generalised Railroad Crossing
Formal Reasoning about Expectation Properties for Continuous Random Variables
Reuse of Verified Design Templates Through Extended Pattern Matching
Deadlock Detection for Actor-Based Coroutines
Safeness of Make-Based Incremental Recompilation
Three Applications of Formal Methods at MITRE
Graphical Development of Consistent System Specifications
A Proof Obligation Generator for VDM-SL
Formal Verification of Multi-Paxos for Distributed Consensus
VDM '91 - Formal Software Development, 4th International Symposium of VDM Europe, Noordwijkerhout, The Netherlands, October 21-25, 1991, Proceedings, Volume 2: Tutorials
Optimal and Robust Controller Synthesis - Using Energy Timed Automata with Uncertainty
Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models
Guess and Verify - Back to the Future
Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code
FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings
The RAISE Toolset
CoVaC: Compiler Validation by Program Analysis of the Cross-Product
Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology
Past, Present, and Future of SRA Implementation of CafeOBJ: Annex
Using PVS to Prove a Z Refinement: A Case Study
Model-Checking the Architectural Design of a Fail-Safe Communication System for Railway Interlocking Systems
Value-Dependent Information-Flow Security on Weak Memory Models
Formal Verification of Operational Transformation
Building VCL Models and Automatically Generating Z Specifications from Them
Software Development and Authentication for Arms Control Information Barriers
DFAMiner: Mining Minimal Separating DFAs from Labelled Samples
Operational Semantics for Model Checking Circus
Operational Semantics of a Weak Memory Model with Channel Synchronization
Automated Test Set Generation for Statecharts
KWIC-index generation
Evidential and Continuous Integration of Software Verification Tools
IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems
Systematic Implementation of Real-Time Models
Specification-Guided Critical Scenario Identification for Automated Driving
Towards an Operational Semantics for Alloy
A Specification of a Complex Programming Language Statement
The Embedded Systems Design Challenge
Model-Based Testing for Avionics Systems
Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings
Using VDM with Rely and Guarantee-Conditions - Experiences from a Real Project
Reformulation: A Way to Combine Dynamic Properties and B Refinement
Strategic Term Rewriting and Its Application to a VDMSL to SQL Conversion
Refactoring Refinement Structure of Event-B Machines
Reasoning about VDM Developments using the VDM Support Tool in MURAL
Multi-robot LTL Planning Under Uncertainty
Extending Isabelle/HOL's Code Generator with Support for the Go Programming Language
Software Security: A Formal Perspective - (Notes for a Talk)
An Industrial Experience on LOTOS-Based Prototyping for Switching Systems Design
Connecting UML and VDM++ with Open Tool Support
Making Temporal Logic Calculational: A Tool for Unification and Discovery
The Probabilistic Termination Tool Amber
Verification of Reactive Systems Using DisCo and PVS
From Complex Specifications to a Working Prototype. A Protocol Engineering Case Study
Systematic Development of Trustworthy Component Systems
Verification Using Test Generation Techniques
Verifying a Distributed Database Lookup Manager Written in Erlang
Well-defined Software Process as Vehicle to Understand Effectiveness of Formal Methods
Forward Simulation for Data Refinement of Classes
Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
On-the-Fly Verification of Linear Temporal Logic
Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks
SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B
A Story About Formal Methods Adoption by a Railway Signaling Manufacturer
Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs
Formal Verification of Transformations for Peephole Optimization
Comparing Correctness-by-Construction with Post-Hoc Verification - A Qualitative User Study
An experimental support system for formal mathematical reasoning
Validation of Mixed SIGNAL-ALPHA Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints
A Formal Framework for Modular Synchronous System Design
Adding Conflict and Confusion to CSP
Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
Maintaining Consistency Under Changes to Formal Specifications
The Role of Modelling in Teaching Formal Methods for Software Engineering
Formal Specification in Metamorphic Programing
What Can Formal Methods Bring to Systems Biology?
EVES: An Overview
Design of Reactive Control Systems for Event-Drivem Operations
Combination of Boxes and Polyhedra Abstractions for Constraint Solving
Informal Strategies in Design by Refinement
Definition, Semantics, and Analysis of Multirate Synchronous AADL
Formal Verification of a C Compiler Front-End
Retrenchment
Formal Specification of a Voice Communication System Used in Air Traffic Control
Formal Development and Verification of a Distributed Railway Control System
Exact and Approximate Strategies for Symmetry Reduction in Model Checking
Looking Back to the Future: Thoughts on Paradigm Shift in Software Development
Compositional Parameter Synthesis
Refinement Semantics and Loop Rules
Towards a Model-Checker for Circus
Variant Analysis with QL
FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings
A Combined Testing and Verification Approach for Software Reliability
Model-Checking TRIO Specifications in SPIN
Combined Online Checking and Control Synthesis: A Study on a Vehicle Platoon Testbed
Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
A Case Study on the Formal Development of a Reactor Safety System
A Survey of Learning Methods in Open Source Software
Formal Verification of Security Properties of Smart Card Embedded Source Code
Switching Controller Synthesis for Hybrid Systems Against STL Formulas
A Model of Specification-Based Testing of Interactive Systems
FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings
Model-Checking of Specifications Integrating Processes, Data and Time
Reasoning About Interactive Systems
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA
A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Specifying Safety and Progress Properties with RSL
On Some Galois Connection Based Abstractions for the Mu-Calculus
Automata Learning through Counterexample Guided Abstraction Refinement
The Integrated Software Development and Verification System ATES
Using Relative Refinement for Fault Tolerance
Verification of a Transactional Memory Manager under Hardware Failures and Restarts
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study
Experiments in Theorem Proving and Model Checking for Protocol Verification
Verifying Consistency and Validity of Formal Specifications by Testing
State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach
Implementing a Model Checker for LEGO
What Have Formal Methods Ever Done for Us? An Audience Discussion
Static Analysis for Detecting High-Level Races in RTOS Kernels
Refinement of State-Based Concurrent Systems
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions
The SRDL Specification Experiment
A Study of Collaborative Work: Answers to a Test on Formal Specification in B
Simulation, Orchestration and Logical Clocks
Do Not Read This
Algebraic Aspects of the Mapping between Abstract Syntax Notation One and CORBA IDL
ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software
Language and Tool Support for Class and State Machine Refinement in UML-B
Exploring Model Quality for ACAS X
A Naive Domain Universe for VDM
From Action Systems to Modular Systems
Semantics-Preserving Simplification of Real-World Firewall Rule Sets
Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach
High Level System Design and Analysis Using Abstract State Machines
Correctness in the Small
A Type Model for VDM
Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic
Towards an Implementation-oriented Specification of TP Protocol in LOTOS
Experience with VDM in Norsk Data
Case Study: Static Security Analysis of the Android Goldfish Kernel
A Translation of Statecharts to Esterel
Abstract Specification of the UBIFS File System for Flash Memory
Gray-Box Monitoring of Hyperproperties
A VDM Subset Compiler
The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications
Towards a Compositional Approach to the Design and Verification of Distributed Systems
Enhancing the Pre- and Postcondition Technique for More Expressive Specifications
An Instrumented Mobile Language Learning Application for the Analysis of Usability and Learning
Disruptive Innovations for the Development and the Deployment of Fault-Free Software
A Strategic Approach to Transformational Design
Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings
MUFFIN: A User Interface Design Experiment for a Theorem Proving Assistant
The UniForM Workbench, a Universal Development Environment for Formal Methods
Two Decades of Formal Methods in Industrial Products at BTC Embedded Systems
Abstract Model Checking without Computing the Abstraction
Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier
FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings
Accurate Static Data Race Detection for C
Combining Real-Time Model-Checking and Fault Tree Analysis
Design of Distributed Multimedia Applications (DAMD)
Reasoning about VDM Specifications
From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET
It's Doomed; We Can Prove It
Helping Programmers to Adopt Set-Based Specifications
A Language for Describing Wireless Mobile Applications with Dynamic Establishment of Multi-way Synchronization Channels
Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System
Modular Extensions to Z
Runtime Verification in Real-Time with the Copilot Language: A Tutorial
Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems
SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis
Proof-Based Development of Specifications with KIDS/VDM
Objectives of the British Standardisation of a Language to support the Vienna Development Method - The BSI VDM Specification Language Standardisation Panel - United Kingdom
Model-Based Security Engineering for Real
Symbolic Animation of JML Specifications
Verification of Unloadable Modules
Certified Memory Usage Analysis
Abstraction and Testing
Software Verification with CPAchecker 3.0: Tutorial and User Guide
Enforcer - Efficient Failure Injection
Abstract Object Creation in Dynamic Logic
Certified Reasoning with Infinity
Formal Verification of Lunar Rover Control Software Using UPPAAL
When Structural Refinement of Components Keeps Temporal Properties over Reconfigurations
A Certified Constraint Solver over Finite Domains
From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
A Fine-Grained Semantics for Arrays and Pointers Under Weak Memory Models
How to Look Next? A Data-Driven Approach for Scanpath Prediction
Formal Methods for Trustworthy Skies: Building Confidence in the Security of Aircraft Assets Distribution
Formal Development of Databases in ASSO and B
Formal Specification and Validation of a Vital Communication Protocol
Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems
A Formal Description of Object-Oriented Programming Using VDM
Trends in Software Verification
Correctness for Beginners
The VIP VDM Specification Language
Finding Minimal Unsatisfiable Cores of Declarative Specifications
Grammar Adaptation
Interference Analysis for Dependable Systems Using Refinement and Abstraction
The IFAD VDM Tools: Lightweight Formal Methods
Symbolic Predictive Analysis for Concurrent Programs
Precise Interval Analysis vs. Parity Games
FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings
Integrating Action Systems and Z in a Medical System Specification
The HP-ST Toolset
L * -Based Learning of Markov Decision Processes
Programming with VDM Domains
Verifying Scenario-Based Aspect Specifications
An Operational Semantics for Timed RAISE
Denotational Semantics of GOTO: An Exit Formulation and Its Relation to Continuations
Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis
Specification and Validation of a Security Policy Model
Upgrading the Pre- and Postcondition Technique
VDM Proof Obligations and their Justification
Using Time to Add Order to Distributed Testing
TLA + Proofs
Composing Temporal-Logic Specifications with Machine Assistance
Timing Analysis of Assembler Code Control-Flow Paths
Automatic Compositional Synthesis of Distributed Systems
Symbolic Model Checking for Distributed Real-Time Systems
Application of a Formal Specification Language in the Development of the "Mobile FeliCa" IC Chip Firmware for Embedding in Mobile Phone
Refining Data to Processes
Executing Formal Semantics with the K Tool
Validation of UML Models Thanks to Z and Lustre
Verifying Dynamic Pointer-Manipulating Threads
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
SpecCert: Specifying and Verifying Hardware-Based Security Enforcement
Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash Table
Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol
Counterexample-Driven Synthesis for Probabilistic Program Sketches
Decentralised LTL Monitoring
Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement
Abstract Model Checking of Infinite Specifications
A Case for Structured Analysis/Formal Design
Applied Formal Methods - FM-Trends 98, International Workshop on Current Trends in Applied Formal Method, Boppard, Germany, October 7-9, 1998, Proceedings
A Simplified Z Semantics for Presentation Interaction Models
Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems
Modeling and Validating Distributed Embedded Real-Time Systems with VDM++
Adding Specification Constructors to the Refinement Calculus
Serialising Parallel Processes in a Hardware/Software Partitioning Context
Secret Ninja Formal Methods
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny
Model Checking Linearizability via Refinement
Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks
Learning Branching-Time Properties in CTL and ATL via Constraint Solving
Mechanized Formal Methods: Where Next?
Comparing Approaches to Data Reification
Applications of Structural Synthesis of Programs
Discourje: Run-Time Verification of Communication Protocols in Clojure - Live at Last
Code-Level Safety Verification for Automated Driving: A Case Study
Equivalence Checking of a Floating-Point Unit Against a High-Level C Model
An Algorithmic Approach to Design Exploration
How to Make FDR Spin LTL Model Checking of CSP by Refinement
The Integration of LOTOS with an Object Oriented Development Method
Compositional Verification of an ATM Protocol
Verifying Smart Contracts with Cubicle
Certificates for Parameterized Model Checking
Archived Design Steps in Temporal Logic
Correctness Proofs for Meta IV Written Code Generator Specification using Term Rewriting
Proceedings of the International Workshop on Web Languages and Formal Methods, WLFM@FM 2005, Newcastle upon Tyne, UK, July 19, 2005
On Excusable and Inexcusable Failures
Efficient Algorithms for Omega-Regular Energy Games
Managerial Issues for the Consideration and Use of Formal Methods
Z and the Refinement Calculus
Automated Boundary Testing from Z and B
veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System
Modular Verification of Programs with Effects and Effect Handlers in Coq
FM-Weck: Containerized Execution of Formal-Methods Tools
Maude as a Formal Meta-tool
Mathematical Modeling and Analysis of an External Memory Manager
Changing Programs Correctly: Refactoring with Specifications
Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems
A Formal Basis for a Program Compilation Proof Tool
Handling Heap Data Structures in Backward Symbolic Execution
Formal Program Development in Geometric Modeling
A Memory Model Sensitive Checker for C#
An Abstract Domain for Objects in Dynamic Programming Languages
An Approach to Unfolding Asynchronous Communication Protocols
QPMC: A Model Checker for Quantum Programs and Protocols
Towards a Verified Model of the Algorand Consensus Protocol in Coq
Automatic Symmetry Detection for Model Checking Using Computational Group Theory
On Combining Functional Verification and Performance Evaluation Using CADP
Formal Aids for the Growth of Software Systems
Formally Verifying Graphics FPU - An Intel® Experience
Model-Based GUI Testing Using Uppaal at Novo Nordisk
The Formal Development of a Secure Transaction Mechanism
How Hard Is Finding Shortest Counter-Example Lassos in Model Checking?
A VDM Study of Fault-Tolerant Stable Storage - Towards a Computer Engineering Mathematics
Verification of the Incremental Merkle Tree Algorithm with Dafny
Verifying Implementation Relations
Verified Software Grand Challenge
Parameter Passing in Algebraic Specification Languages
Examples of the Application of Formal Methods to Interactive Systems
Property-Driven Fence Insertion Using Reorder Bounded Model Checking
A Tableau for CTL
Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way
Free Facts: An Alternative to Inefficient Axioms in Dafny
Reconciling Real-Time with Asynchronous Message Passing
No Risk, No Fun - A Tutorial on Risk Management
Unification in Matching Logic
An Algebraic Approach to Refinement
Formalisation and Implementation of Road Junction Rules on an Autonomous Vehicle Modelled as an Agent
Checking Well-Formedness of Pure-Method Specifications
Heuristic-Driven Test Case Selection from Formal Specifications. A Case Study
Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Writing Simulatable Specifications in SPECIAL
Conformity Clause for VDM-SL
On Failures and Faults
B-Tool
Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison
An Action Semantics for ML Concurrency Primitives
Automated Repair of Information Flow Security in Android Implicit Inter-App Communication
Critical Systems Validation and Verification with CSP and FDR
A Symbolic Algorithm for the Analysis of Robust Timed Automata
Combining Tools for Optimization and Analysis of Floating-Point Computations
Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
A Framework for Correctness Criteria on Weak Memory Models
Automated Verification of RPC Stub Code
Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification
Sound and Complete Mutation-Based Program Repair
Verifying Linearisability with Potential Linearisation Points
A Uniform Approach for the Definition of Security Properties
Improvements in Coverability Analysis
Probabilistic Bisimulation for Realistic Schedulers
Challenges Faced by Students in an Open Source Software Undergraduate Course
Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination
Software Support for the Refinement of VDM Specifications
FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings
Using VDM in an Object-Oriented Development Method for Ada Software
Fair Model Checking with Process Counter Abstraction
IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems
Verifying Secure Speculation in Isabelle/HOL
Efficient Self-composition for Weakest Precondition Calculi
Formal Verification of a Descent Guidance Control Program of a Lunar Lander
Tutorial on the Irish School of the VDM
Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol
Semantics of First Order Parametric Specifications
Formal and Informal Specifications of a Secure System Component: Final Results in a Comparative Study
Formal Methods for Privacy
"Know Thyself" How Personal Music Tastes Shape the Last.Fm Online Social Network
The RAISE Specification Langiage: A Tutorial
An Attempt to Reason about Shared-State Concurrency in the Style of VDM
Towards a Method for the Decomposition by Refinement in Event-B
Visualizing Game-Based Certificates for Hyperproperty Verification
On Combining State Space Reductions with Global Fairness Assumptions
Using Real-Time Maude to Model Check Energy Consumption Behavior
Combining CSP and B for Specification and Property Verification
The ScalaFix Equation Solver
Formal Specification and Verification of the pGVT Algorithm
A Formal Semantics for a DataFlow Machine - Using VDM
An Approach to the Static Semantics of VDM-SL
Integrating Real-Time Scheduling Theory and Program Refinement
Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning