yusuke1997/dblp-id-title huggingface dataset:
Automated Anonymity Verification of the ThreeBallot Voting System
Stateful Behavioral Types for Active Objects
Compositional Verification of Software Product Lines
An Integrated Approach to a Combinatorial Optimisation Problem
PyQBF: A Python Framework for Solving Quantified Boolean Formulas
Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System
State/Event-Based Software Model Checking
Stateful Functional Modeling with Refinement (a Lean4 Framework)
Probabilistic Timed Behavior Trees
Linking CSP-OZ with UML and Java: A Case Study
UML to B: Formal Verification of Object-Oriented Models
State/Event Software Verification for Branching-Time Specifications
Integrated Formal Methods, 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings
A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms
Combining Graphical and Formal Development of Open Distributed Systems
Knowledge for the Distributed Implementation of Constrained Systems
Simple Dependent Types for OSTRICH
Integrating Software and Hardware Verification
Bug Hunting with False Negatives
Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction
A Formal Model of the Safety-Critical Java Level 2 Paradigm
Analysis of Synchronisations in Stateful Active Objects
Early Fault Detection in Industry Using Models at Various Abstraction Levels
Operation Caching and State Compression for Model Checking of High-Level Models - How to Have Your Cake and Eat It
Certified Password Quality - A Case Study Using Coq and Linux Pluggable Authentication Modules
Towards Generating SPARK from Event-B Models
A CSP Approach to Control in Event-B
A Compositional Automata-Based Semantics for Property Patterns
Reasoning About Exceptional Behavior at the Level of Java Bytecode
Efficient CSP Z Data Abstraction
Integrated Formal Methods - 20th International Conference, iFM 2025, Paris, France, November 19-21, 2025, Proceedings
Studying Users' Willingness to Use a Formally Verified Password Manager
The Digital Thread in Industry 4.0
Verifying Behavioral UML Systems via CEGAR
From Z to B and then Event-B: Assigning Proofs to Meaningful Programs
Qualitative Probabilistic Modelling in Event-B
Integrated Formal Methods, Third International Conference, IFM 2002, Turku, Finland, May 15-18, 2002, Proceedings
A Policy Language to Capture Compliance of Data Protection Requirements
Structural Transformations for Data-Enriched Real-Time Systems
Basic-REAL: Integrated Approach for Design, Specification and Verification of Distributed Systems
Automated Sensitivity Analysis for Probabilistic Loops
Characterizing Fault-Tolerant Systems by Means of Simulation Relations
Reachability Analysis of Function-as-a-Service Scheduling Policies
A Tutorial Introduction to Designs in Unifying Theories of Programming
Design and Verification of Restart-Robust Industrial Control Software
Towards Real-Time Object-Z
A Hybrid Analysis for Security Protocols with State
Grey-Box Learning of Register Automata
Multiformalism and Transformation Inheritance for Dependability Analysis of Critical Systems
Verify This: Memcached - A Practical Long-Term Challenge for the Integration of Formal Methods
Symbolic Computation and Automated Reasoning for Program Analysis
Resource Sharing via Capability-Based Multiparty Session Types
iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings
Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods
Translating Hardware Process Algebras into Standard Process Algebras: Illustration with CHP and LOTOS
Reusing Predicate Precision in Value Analysis
Formalizing Timing Diagrams as Causal Dependencies for Verification Purposes
Towards Probabilistic Modelling in Event-B
Model Checking Buffered Durable Linearizability in CSP
Contribution to a Rigorous Analysis of Web Application Frameworks
Automatic Verification of Parametric Specifications with Complex Topologies
Translating Statecharts to B
Taming the Unbounded for Hardware Synthesis
Fuzzing JavaScript Environment APIs with Interdependent Function Calls
Exploring LLMs and Semantic XAI for Industrial Robot Capabilities and Manufacturing Commonsense Knowledge
ISpec: Towards Practical and Sound Interface Specifications
Auto-Generating Visual Editors for Formal Logics with Blockly
Integrated Formal Methods, Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 1-3, 2000, Proceedings
Verifying Smart Card Applications: An ASM Approach
Extending Data Flow Coverage to Test Constraint Refinements
Formal Verification of PKCS#1 Signature Parser Using Frama-C
Integrating Event-B Modelling and Discrete-Event Simulation to Analyse Resilience of Data Stores in the Cloud
Adaptive Techniques for Specification Matching in Embedded Systems: A Comparative Study
Integrated Formal Methods, Proceedings of the 1st International Conference on Integrated Formal Methods, IFM 99, York, UK, 28-29 June 1999
Ontology-Mediated Probabilistic Model Checking
Probabilistic Formal Analysis of App Usage to Inform Redesign
Chain of Events: Modular Process Models for the Law
Using Bayesian Inference and Flowpipe Construction to Bound Predictions of Biogas Production at Wastewater Treatment Plants
Proving Linearizability Via Non-atomic Refinement
Verifying Modal Workflow Specifications Using Constraint Solving
Creating Sequential Programs from Event-B Models
Avoiding Medication Conflicts for Patients with Multimorbidities
Generalised Test Tables: A Practical Specification Language for Reactive Systems
Visualization and Abstractions for Execution Paths in Model-Based Software Testing
Modelling and Verification for Swarm Robotics
Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B
Kaki: Concurrent Update Synthesis for Regular Policies via Petri Games
Mechanized Extraction of Topology Anti-patterns in Wireless Networks
Modular Verification of Dynamic Properties for Reactive Systems
Integration Problems in Telephone Feature Requirements
A Compositional Comparison of Specifications of the Alternating Bit Protocol in CCS and UNITY Based on Algebra Transformation Systems
Formal Verification of Compiler Transformations on Polychronous Equations
HyperPCTL Model Checking by Probabilistic Decomposition
Automated Verification of Security Policies in Mobile Code
Axiomatic Characterization of Trace Reachability for Concurrent Objects
VeriCode: Correct Translation of Abstract Specifications to C Code
Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods
Lifting the Reasoning Level in Generic Weak Memory Verification
Monitoring Real-Time Systems Under Parametric Delay
Making Whiley Boogie!
Finding State Solutions to Temporal Logic Queries
On Implementing a Monitor-Oriented Programming Framework for Actor Systems
Verifying Autonomous Systems
CloudSDV Enabling Static Driver Verifier Using Microsoft Azure
A Fixpoint Semantics of Event Systems With and Without Fairness Assumptions
Formal Specification and Verification of JDK's Identity Hash Map Implementation
Software Verification with Integrated Data Type Refinement for Integer Arithmetic
Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA
Mechanised Translation of Control Law Diagrams into Circus
Symbolic Model-Checking of Optimistic Replication Algorithms
Enabling Security Testing from Specification to Code
Modelling Discrete Behaviour in a Continuous-Time Formalism
Robotics and Integrated Formal Methods: Necessity Meets Opportunity
Conservative Time Discretization: A Comparative Study
Task Planning with OMT: An Application to Production Logistics
A Constraint Satisfaction Method for Configuring Non-local Service Interfaces
Hybrid Games with Triggers
Modular Verification for a Class of PLTL Properties
Jaint: A Framework for User-Defined Dynamic Taint-Analyses Based on Dynamic Symbolic Execution of Java Programs
Reasoning About JML: Differences Between KeY and OpenJML
Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
Detection of Polluting Test Objectives for Dataflow Criteria
Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata
Minimally and Maximally Abstract Retrenchments
Behaviour-Based Cheat Detection in Multiplayer Games with Event-B
Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings
Application of Graph Transformation in Verification of Dynamic Systems
Decompositional Petri Net Reductions
Facilitating the Implementation of Distributed Systems with Heterogeneous Interactions
Triggerless Happy - Intermediate Verification with a First-Order Prover
Formal Modeling of Trust in Autonomous Delivery Vehicles
Property Specifications for Workflow Modelling
Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings
Improved Reachability Analysis in DTMC via Divide and Conquer
An Introduction to Grammar Convergence
Verification Architectures: Compositional Reasoning for Real-Time Systems
Developing Control Systems Components
A Compositional Method for Deciding Equivalence and Termination of Nondeterministic Programs
Contributions for Modelling UML State-Charts in B
Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings
Practical Abstractions for Automated Verification of Message Passing Concurrency
Incremental Reasoning for Multiple Inheritance
Integrating Implicit Induction Proofs into Certified Proof Environments
Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL
Verifying UML/OCL Operation Contracts
The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification
How to Break the Bank: Semantics of Capability Policies
Meeduse: A Tool to Build and Run Proved DSLs
Translating FSP into LOTOS and Networks of Automata
Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion
Formally Linking MDG and HOL Based on a Verified MDG System
Formal Modelling and Verification of Population Protocols
Model-Checking CSP-OZ Specifications with FDR
An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems
Agile Formal Method Engineering
Towards Formal Verification of a TPM Software Stack
Using Ontologies in Formal Developments Targeting Certification
Retrenchment and Punctured Simulation
A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
Detecting Vulnerabilities in Java-Card Bytecode Verifiers Using Model-Based Testing
An Interactive Verification Tool Meets an IDE
Making Linearizability Compositional for Partially Ordered Executions
Reasoning About Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems
Behavioural Specifications from Class Models
Specifying Interactive Systems in Object-Z and CSP
Integrated Formal Methods, 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005, Proceedings
A Precise Pictorial Language for Array Invariants
Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System
Isomorphic Transfer Infrastructure for Nested Types in Isabelle/HOL (Work in Progress)
mu-Charts and Z: Hows, Whys, and Wherefores
BTS: A Tool for Formal Component-Based Development
Developing Topology Discovery in Event-B
Combining Static Analysis and Testing for Deadlock Detection
CHC Model Validation with Proof Guarantees
Consistency in UML and B Multi-view Specifications
Deadlock Analysis of Concurrent Objects: Theory and Practice
Quantified Abstractions of Distributed Systems
Combining Operational Semantics, Logic Programming and Literate Programming in the Specification and Animation of the Verilog Hardware Description Language
Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch
A Dialogue Interface for Low Code Program Evolution
Machine-Assisted Proofs for Institutions in Coq
Proving Termination via Measure Transfer in Equivalence Checking
Reformulation of SAT into a Polynomial Box-Constrained Optimization Problem
The Refinement of Event Calculus Models
Unfolding Iterators: Specification and Verification of Higher-Order Iterators in OCaml
A Requirements-Driven Methodology: Formal Modelling and Verification of an Aircraft Engine Controller
Formal Verification of Legal Contracts: A Translation-Based Approach
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata
Quick Theory Exploration for Algebraic Data Types via Program Transformations
An Approach to the Combination of Formal Description Techniques: Statecharts and TLA
CHC-Based Reachability Analysis via Cycle Summarization
Object-Oriented Modelling with High-Level Modular Petri Nets
Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics
Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings
A Process Compensation Language
Verifying Temporal Properties of CommUnity Designs
Integrated Formal Methods - 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings
Extended Abstract: Skill-Based Architectures in Autonomous Systems: Lessons Learnt
Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples
Development of Fault Tolerant Grid Applications Using Distributed B
Monitoring Multi-threaded Component-Based Systems
An Automated Failure Mode and Effect Analysis Based on High-Level Design Specification with Behavior Trees
Deductive Reasoning versus Model Checking: Two Formal Approaches for System Development
Formal Methods for GPGPU Programming: Is the Demand Met?
On the Industrial Uptake of Formal Methods in the Railway Domain - A Survey with Stakeholders
A Formal Semantics for Complete UML State Machines with Communications
Assume-Guarantee Algorithms for Automatic Detection of Software Failures
A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset
History-Based Specification and Verification of Java Collections in KeY
Rule-Based Consistency Checking of Railway Infrastructure Designs
VBPMN: Automated Verification of BPMN Processes (Tool Paper)
Modeling UML Template Classes with FoCaLiZe
Online Model Checking for Anomaly Detection in Industrial Control Systems
Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings
Integration of Specification Languages Using Viewpoints
Game Modeling of Blockchain Protocols
Clustering-Guided SMT($\mathcal {L\!R\!A}$) Learning
Towards Quantitative Analysis of Simulink Models Using Stochastic Hybrid Automata
Why Just Boogie? - Translating Between Intermediate Verification Languages
Learning Finite State Models fromRecurrent Neural Networks
Correct and Complete Symbolic Execution for Free
Integrated Static Analysis for Linux Device Driver Verification
StEVe: A Rational Verification Tool for Stackelberg Security Games
Combining Mobility with State
Specification and Analysis of Automata-Based Designs
Verifying Linearizability on TSO Architectures
Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL
Safety and Line Capacity in Railways - An Approach in Timed CSP
Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption
Modelling and Verification of Timed Robotic Controllers
Adding Change Impact Analysis to the Formal Verification of C Programs
Mode-Aware Concolic Testing for PLC Software - Special Session "Formal Methods for the Design and Analysis of Automated Production Systems"
A Proof Framework for Concurrent Programs
UTP Semantics for Web Services
SAL-Based Symbolic Scheduling in Time-Triggered Networks
Synthesizing Clock-Efficient Timed Automata
Translating VDM to Alloy
Model-Checking Software Library API Usage Rules
Using a Process Algebra to Control B Operations
Probabilistic Model Checking of BPMN Processes at Runtime
Enhancing Automata Learning by Log-Based Metrics
Verification of EB 3 Specifications Using CADP
Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
SNITCH: A Platform for Information Flow Control
Task-Node Mapping in an Arbitrary Computer Network Using SMT Solver
Formalization of Cadence SPW Fixed-Point Arithmetic in HOL
When Separation Arithmetic is Enough
Analysing AWN-Specifications Using mCRL2 (Extended Abstract)
Active Objects with Deterministic Behaviour
Extending Timed Automata with Clock Derivatives
Structural Refinement in Object-Z/CSP
Sound Probabilistic Numerical Error Analysis
Dynamic Path Reduction for Software Model Checking
Using UML Sequence Diagrams as the Basis for a Formal Test Description Language
Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation
Modeling Register Pairs in CompCert
SMT: Something You Must Try
Priced Timed Automata and Statistical Model Checking
Model Checking Object-Z Using ASM
Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays
Formal Security Analysis of the MaCAN Protocol
A Concurrent and Compositional Petri Net Semantics of Preemption
Refinement and Separation: Modular Verification of Wandering Trees
Formal Refinement in SysML
Fast and Effective Well-Definedness Checking
Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors
Co-simulation of Distributed Embedded Real-Time Control Systems
Algebraic Compilation of Safety-Critical Java Bytecode
Security of the Lightning Network: Model Checking a Stepwise Refinement with TLA +
Integrated Formal Methods, 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16-19, 2009. Proceedings
Synthesizing Coalitions for Multi-agent Games
SemSlice: Exploiting Relational Verification for Automatic Program Slicing
Asynchronous Testing of Synchronous Components in GALS Systems
Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication
Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming
Stochastic Process Algebras Meet Eden
Patterns for a Log-Based Strengthening of Declarative Compliance Models
The Design of a Tool-Supported Graphical Notation for Timed CSP
The VerCors Tool Set: Verification of Parallel and Concurrent Software
MULE-Based Wireless Sensor Networks: Probabilistic Modeling and Quantitative Analysis
Structuring Real-Time Object-Z Specifications
Towards Correct-by-Construction Machine-Learnt Models
A Logical Framework to Deal with Variability
Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study -
Slicing Concurrent Real-Time System Specifications for Verification
Inheriting Laws for Processes with States
Why Doesn't Anyone Use Formal Methods?
Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function
Towards a Unified Development Methodology for Shared-Variable Parallel and Distributed Programs
Broadcast, Denial-of-Service, and Secure Communication
Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin
Systematic Translation Rules from astd to Event-B
An Event-B Approach to Data Sharing Agreements
Summary of: On Checking Delta-Oriented Software Product Lines of Statecharts
Model Checking LTL Formulae in RAISE with FDR
Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems
Algebra-Based Loop Synthesis
An Extension of the ABS Toolchain with a Mechanism for Type Checking SPLs
Testing and Verifying Chain Repair Methods for Corfu Using Stateless Model Checking
Specification and Verification of Model Transformations Using UML-RSDS
Combining Quantitative and Qualitative Analysis for Safe and Resilient Intelligent Hybrid Systems
Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints
Towards Logical Specification and Checking of Evasive Malware
Understanding Object-Z Operations as Generalised Substitutions
Verifying Pointer Programs Using Separation Logic and Invariant Based Programming in Isabelle
Partial Order Reduction for State/Event LTL
Formal Verification of CNL Health Recommendations
Non-interference Properties for Data-Type Reduction of Communicating Systems
Software Model Checking: Searching for Computations in the Abstract or the Concrete
Integrating Model Checking and Theorem Proving in a Reflective Functional Language
Property Preservation for Extension Patterns of State Transition Diagrams
A Modular Framework for the Integration of Heterogeneous Notations and Tools
Modular Formal Specification of Data and Behaviour
Branching Temporal Logic of Calls and Returns for Pushdown Systems
Challenges in the Specification of Full Contracts
Model-Based Prototyping of an Interoperability Protocol for Mobile Ad-Hoc Networks
Challenges in Autonomous Robotic System Verification
Design Verification for Control Engineering
Predicate Abstraction in a Program Logic Calculus
Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings
Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B
Fuzzing JavaScript Engine APIs
Verification of Multi-agent Negotiations Using the Alloy Analyzer
Hoare-Style Reasoning from Multiple Contracts
Requirements for a Temporal B - Assigning Temporal Meaning to Abstract Machines... and to Abstract Systems
A Multi-target Code Generator for High-Level B
Probabilistic Verification of Timing Constraints in Automotive Systems Using UPPAAL-SMC
Managing LTL Properties in Event-B Refinement
SMT Solvers for Validation of B and Event-B Models
From Small-Step Semantics to Big-Step Semantics, Automatically
Formal Modelling and Analysis of a Self-Adaptive Robotic System
Learning to Reuse: Adaptive Model Learning for Evolving Systems
Shuffling Posets on Trajectories
Analysis and Formal Specification of OpenJDK's BitSet
Formal Verification Based on Guided Random Walks
Refinement in Object-Z and CSP
An Object Semantic Model of SOFL
Cooperation of Formal Methods in an Engineering Based Software Development Process
Programming with Miracles
Empowering the Event-B Method Using External Theories
Modular Verification of Order-Preserving Write-Back Caches
Can Formal Methods Improve the Efficiency of Code Reviews?
Symbolic Model Checking of Relative Safety LTL Properties
RT-Z: An Integration of Z and timed CSP
Towards a Formal Notion of Impact Metric for Cyber-Physical Attacks
Code Generation for Event-B
How Well Can I Secure My System?
Proofs and Refutations in Invariant-Based Programming
A Framework for Translating Models and Specifications
Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method
CZT Support for Z Extensions
Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods
A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress)
Lifting General Correctness into Partial Correctness is ok
Systems Design Guided by Progress Concerns
Automatic Inference of Erlang Module Behaviour
Validating Z Specifications Using the ProBAnimator and Model Checker
PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases
Construction of Finite Labelled Transistion Systems from B Abstract Systems
Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems
Computing Bisimilarity Metrics for Probabilistic Timed Automata
CAN-verify: A Verification Tool For BDI Agents
Realizability of Choreographies Using Process Algebra Encodings
Behavioral Conformance Verification in an Integrated Approach Using UML and B
Model Checking as Static Analysis: Revisited
VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory
A Generalised Theory of Interface Automata, Component Compatibility and Error
Towards a Formal Semantics-Based Technique for Interprocedural Slicing
Monitoring Extended Hypernode Logic