yusuke1997/dblp-id-title huggingface dataset:
An Abstract Semantics of Speculative Execution for Reasoning About Security Vulnerabilities
AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned
Lazy Behavioral Subtyping
Secure Interoperation of Secure Distributed Databases
Systems Development Using Z Generics
Using Z as a Specification Calculus for Object-Oriented Systems
Smart Contracts: Application Scenarios for Deductive Program Verification
A Specification Language
An Algebraic Framework for Higher-Order Modules
Formal Methods in the Railways Signalling Industry
Error Detection with Directed Symbolic Model Checking
Houdini, an Annotation Assistant for ESC/Java
Non-atomic Refinement in Z
Validating B, Z and TLA + Using ProB and Kodkod
On Software Safety, Security, and Abstract Interpretation
Semantics of BPEL4WS-Like Fault and Compensation Handling
A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software
A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
TraceContract: A Scala DSL for Trace Analysis
A Calculus of Chaos in Stochastic Compilation - Engineering in the Cause of Mathematics
A Weakest Precondition Semantics for an Object-Oriented Language of Refinement
Deductive Proof of Industrial Smart Contracts Using Why3
A Strategy for the Production of Verifiable Code Using the B Method
Proofs of Correctness of Cache-Coherence Protocols
Properties of Behavioural Model Merging
Avoiding State Explosion for Distributed Systems with Timestamps
Verification Techniques for LOTOS
Backdoor Mitigation in Deep Neural Networks via Strategic Retraining
Components, Contracts, and Connectors for the Unified Modelling Language UML
Weakening Correctness and Linearizability for Concurrent Objects on Multicore Processors
Interactive Design and Verification: A Message Switching Network Example
Embedding High-Level Formal Specifications into Applications
Static Differential Program Analysis for Software-Defined Networks
The Safety-Critical Java Memory Model: A Formal Account
Cache Coherence Verification with TLA+
The Modal Transition System Control Problem
HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic
The Larch Approach to Specification (Abstract)
Type-Safe Two-Level Data Transformation
Secure Synthesis of Code: A Process Improvement Experiment
RTL and Refutation by Positive Cycles
Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II
Interactive Verification of Medical Guidelines
Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
A Formal Approach to Autonomous Vehicle Coordination
Log Analysis for Data Protection Accountability
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization
An Open Environment for the Integration of Hetereogenous Modelling Techniques and Tools
B2SAT: A Bare-Metal Reduction of B to SAT
Staged Specification Logic for Verifying Higher-Order Imperative Programs
Efficient Tight Field Bounds Computation Based on Shape Predicates
A Theory of Presentations
Gender Recognition in the Wild with Small Sample Size - A Dictionary Learning Approach
The Next Big Thing: From Embedded Systems to Embodied Actors
Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies
A Behavioral Model for Co-design
Analyzing the Restart Behavior of Industrial Control Applications
Interlocking Design Automation Using Prover Trident
A Compositional Proof System for Shared Variable Concurrency
Foundations of Semantics and Model Checking in a Software Engineering Course
Discounted Duration Calculus
sfPFL: A Probabilistic Logic for Fault Trees
Formal Specification and Verification of Dynamic Parametrized Architectures
UniTesK Test Suite Architecture
A Support System for Formal Reasoning: Requirements and Status
VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs
Local Nondeterminism in Asynchronously Communicating Processes
Abstraction and Subsumption in Modular Verification of C Programs
Formal Specification of a Cardiac Pacing System
Supplementing a UML Development Process with B
Emma: Developing an Industrial Reachability Analyser for SDL
Formal Modelling and Simulation of Train Control Systems Using Petri Nets
Does It Pay to Extend the Perimeter of a World Model?
A Model Checking Language for Concurrent Value-Passing Systems
Privacy by Design in Practice: Reasoning about Privacy Properties of Biometric System Architectures
Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods
A Systematic Approach to Automotive Security
Bunches for Object-Oriented, Concurrent, and Real-Time Specification
TLA + PROMELA: Conjecture, Check, Proof, Engineering New Protocols Using Methods and Formal Notations
Learning Deterministic Variable Automata over Infinite Alphabets
Timed Testing with TorX
Understanding Synthesized Reactive Systems Through Invariants
Compositional Reasoning for Shared-Variable Concurrent Programs
Regression Verification for Unbalanced Recursive Functions
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs
Unifying Probability with Nondeterminism
Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers
Specification and Refinement in an Integrated Database Application Environment
Model Checking for Verification of Quantum Circuits
Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation
Using RAISE - First Impressions from the LaCoS Applications
Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
Can We Communicate? Using Dynamic Logic to Verify Team Automata
Certifiable Specification and Verification of C Programs
Proving Functional Program Equivalence via Directed Lemma Synthesis
The Safe Machine: A New Specification Construct for B
Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics
Automated Real Proving in PVS via MetiTarski
The wHOLe System
Compositional Symmetric Sharing in B
Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets
The School of Squiggol - A History of the Bird-Meertens Formalism
Reification of Executable Test Scripts in Formal Specicifation-Based Test Generation: The Java Card Transaction Mechanism Case Study
Towards a Formalization of Programming-by-Difference
Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP
Formalising British Rail's Signalling Rules
Procedure-Level Verification of Real-time Concurrent Systems
Different FDT's Confronted with Different ODP-Viewpoints of the Trader
A Pyramid Of (Formal) Software Verification
An Extended VDM Refinement Relation
On transferring VDM verification techniques to Z
Flexible and Reliable Process Model Properties: An Integrated Approach
Z3 and SMT in Industrial R&D
Modeling Aircraft Mission Computer Task Rates
Determining the Specification of a Control System from That of Its Environment
Safety Analysis in Formal Specification
Approximate Bisimulation and Discretization of Hybrid CSP
Structured Specifications for Better Verification of Heap-Manipulating Programs
Behavioural Extension for CSP
A Timed Semantics for the STATEMATE Implementation of Statecharts
A PVS-Based Approach for Teaching Constructing Correct Iterations
Structuring for the VDM Specification Language
A Termination Detection Algorithm: Specification and Verification
Fortune Nets for Fortunettes: Formal, Petri Nets-Based, Engineering of Feedforward for GUI Widgets
Formal Development of a Serial Copy Management System
Efficient SMT-Based Network Fault Tolerance Verification
Experience from Applications of RAISE
Test Criteria Definition for B Models
Timed Migration and Interaction with Access Permissions
symQV: Automated Symbolic Verification of Quantum Programs
Synthesis of Distributed Processes from Scenario-Based Specifications
Towards the Semantics of the Definitional Language of MetaSoft
Applying the B Technologies on CICS
A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes
FME '94: Industrial Benefit of Formal Methods, Second International Symposium of Formal Methods Europe, Barcelona, Spain, October 24-18, 1994, Proceedings
An Industrial Case: Pitfalls and Benefits of Applying Formal Methods to the Development of a Network-Centric RTOS
The Bourgeois Gentleman, Engineering and Formal Methods
Finding Suitable Variability Abstractions for Family-Based Analysis
The Denotational Semantics of slotted-Circus
Two-Way Quantum and Classical Automata with Advice for Online Minimization Problems
Circus2CSP: A Tool for Model-Checking Circus Using FDR
Counter-Example Guided Program Verification
Formal Methods Reality Check: Industrial Usage
Narrowing Operators on Template Abstract Domains
Formal Management of CAD/CAM Processes
Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN
The Formal Classification and Verification of Simpson's 4-Slot Asynchronous Communication Mechanism
Diagnosing Industrial Business Processes: Early Experiences
Formal Methods Applicability on Space Applications Specification and Implementation Using MORA-TSP
Automatically Refining Partial Specifications for Program Verification
Using VDM within an Object-Oriented Framework
Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle
A More Complete TLA
SOA and the Button Problem
NUSL: An Executable Specification Language Based on Data Abstraction
Relational Reasoning via SMT Solving
A Lightweight Approach to Formal Methods
Sampling-Based Runtime Verification
Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking
Resource-Aware Design for Reliable Autonomous Applications with Multiple Periods
Reduced Execution Semantics of MPI: From Theory to Practice
Modelling Human Reasoning in Practical Behavioural Contexts Using Real-Time Maude
Advancing Quantum Computing with Formal Methods
Nested Event Representation for Automated Assembly of Cell Signaling Network Models
Experience Using VDM in STC
Formal Analysis of Neural Network-Based Systems in the Aircraft Domain
Reasoning About Promises in Weak Memory Models with Event Structures
Management of Time Requirements in Component-Based Systems
Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project
The Octatope Abstract Domain for Verification of Neural Networks
A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems
Consistent Graphical Specification of Distributed Systems
Structuring Retrenchments in B by Decomposition
Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers
Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems
Verification of Fair Controllers for Urban Traffic Manoeuvres at Intersections
An Overview of RDM: Rational Design Methodology
Integration, the Price of Success
Synthesizing Certified Code
Using Domain-Independent Problems for Introducing Formal Methods
Recursive Definitions of Operations in Universal Algebras
Model Checking FTA
A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
Formal Verification of Consensus in the Taurus Distributed Database
View Abstraction for Systems with Component Identities
Integrating ADTs in KeY and Their Application to History-Based Reasoning
Eliminating Static Analysis False Positives Using Loop Abstraction and Bounded Model Checking
TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms
Modular Verification of Static Class Invariants
The Opacity of Timed Automata
Three-Valued Predicates for Software Specification and Validation
Formal Modelling and Verification as Rigorous Review Technology: An Inspiration from INSPEX
On the Formalization of Programming Languages: Early History and Main Approaches
A Graphic Notation for Formal Specifications of Dynamic Systems
Type Checking BSI/VDM-SL
Abstraction and Refinement in RDM
On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study
Towards a Static Check of FMUs in VDM-SL
A Precise Examination of the Behaviour of Process Models
A Formal Security Model for Microprocessor Hardware
Verifying Functional Correctness Properties at the Level of Java Bytecode
An Introduction to Refinement in Z
Improvements in BDD-Based Reachability Analysis of Timed Automata
Monitoring the Internet Computer
Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections
Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
A Buffering System Implementation using VDM
Formal Modeling of the Enterprise JavaBeans TM Component Integration Framework
Role of VDM(++) in the Development of a Real-Time Tracking and Tracing System
Refining Action Systems within B-Tool
Combining VDM-SL Specifications with C++ Code
A Model Checking Approach to Discrete Bifurcation Analysis
A Fully Verified Container Library
CauMon: An Informative Online Monitor for Signal Temporal Logic
Diagrams and Programming Languages for Programmable Controllers
Selling Formal Methods to Industry
State Matching and Multiple References in Adaptive Active Automata Learning
The Java Verification Tool KeY:A Tutorial
Two Refinement Case Studies
A Critical Look at Functional Specifications
Semantic Web for Extending and Linking Formalisms
Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning
An Integrated Approach to Specification and Validation of Real-Time Systems
Report from the BSIPanel for the Standardisation of VDM (IST/5/50)
FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings
HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams
The B Tool (Abstract)
Team Automata Satisfying Compositionality
Measles Epidemics and PEPA: An Exploration of Historic Disease Dynamics Using Process Algebra
Formalizing Design Spaces: Implicit Invocation Mechanisms
Local Planning of Multiparty Interactions with Bounded Horizons
A Minimal Framework for Specification Theory
An Example of Use of Formal Methods to Debug an Embedded Software
FME '96: Industrial Benefit and Advances in Formal Methods, Third International Symposium of Formal Methods Europe, Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18-22, 1996, Proceedings
Towards 'Verifying' a Water Treatment System
Compositional Class Refinement in Object-Z
PICGAL: Practical Use of Formal Specification to Develop a Complex Critical System
Combining Forces: How to Formally Verify Informally Defined Embedded Systems
SMPT: A Testbed for Reachability Methods in Generalized Petri Nets
Improving JML: For a Safer and More Effective Language
MURAL and SPECBOX
Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I
On Partitioning and Symbolic Model Checking
Verification of Cryptographic Protocols: An Experiment
Data Reification without Explicit Abstraction Functions
The Use of VDM in the Specification of Chinese Characters
An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method
Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems
Experience Report on Designing and Developing Control Components Using Formal Methods
Gaussian Process-Based Confidence Estimation for Hybrid System Falsification
Statistical Model Checking of LLVM Code
Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings
Practices for Formal Models as Documents: Evolution of VDM Application to "Mobile FeliCa" IC Chip Firmware
Recovering High-Level Conditions from Binary Programs
Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs
Using Debuggers to Understand Failed Verification Attempts
Model-Based Design of an Energy-System Embedded Controller Using Taste
Error Invariants for Concurrent Traces
Recursive Definitions Revisited
Probabilistic Polynomial-Time Equivalence and Security Analysis
The Industrial Take-up of Formal Methods in Safety-Critical and Other Areas: A Perspective
Developing Components in the Presence of Re-entrance
Revisiting Compatibility of Input-Output Modal Transition Systems
Model-Checking over Multi-valued Logics
An Overview of the SPRINT Method
Software Abstraction Principles: Tutorial Examples of: An Operating System Command Language Specification, and a PL/I-like On-Condition Language Definition
A TLA Solution to the Specification and Verification of the RLP1 Retransmission Protocol
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service
VDM Development with ADA as the Target Language
Deduction in the Verification Support Environment (VSE)
Timed Vacuity
Abstract Execution
Formalizing and Verifying a Modern Build Language
Resource Analysis: From Sequential to Concurrent and Distributed Programs
Using Formal Verification Techniques to Reduce Simulation and Test Effort
Quantitative Analysis of an Application of Formal Methods
Smart Contract Interactions in Coq
The Mondex Challenge: Machine Checked Proofs for an Electronic Purse
Integrating Loop Acceleration Into Bounded Model Checking
IPL: An Integration Property Language for Multi-model Cyber-physical Systems
Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes
The Vienna Development Method: The Meta-Language
Compiler Prototyping with VDM and Standard ML
Formal Virtual Modelling and Data Verification for Supervision Systems
Lightweight Formal Methods
Compositional Verification of Concurrent Systems by Combining Bisimulations
VDM in Three Generations of Ada* Formal Descriptions
Reachability Analysis of the HTML5 Parser Specification and Its Application to Compatibility Testing
Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms
Specification by Data Types
The Stepwise Development of Software Development Graphs: Meta-Programming VDM Developments
An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor
Data Reification and Program Decomposition
Recursive Abstractions for Parameterized Systems
Towards an Integrated Model Checker for Railway Signalling Data
A Case Study on Formal Equivalence Verification Between a C/C++ Model and Its RTL Design
On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery
FME '93: Industrial-Strength Formal Methods, First International Symposium of Formal Methods Europe, Odense, Denmark, April 19-23, 1993, Proceedings
Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs
Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts
Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case Study
FSM Inference from Long Traces
Word Equations in Synergy with Regular Constraints
Verifying Emulation of Legacy Mission Computer Systems
A Programming Model for Wide-Area Computing
Unifying Weak Memory Verification Using Potentials
Application of Composition Development Method for definition of SYNTHESIS information resource query language semantics
SDN-Actors: Modeling and Verification of SDN Programs
20 Years of Real Real Time Model Validation
Support Environments for VDM
Verifying Correctness of Persistent Concurrent Data Structures
Formal Methods in Standards - A Report from the BCS Working Group
Use of VDM within CCITT
Anomaly Detection from Log Files Using Unsupervised Deep Learning
PSL Model Checking and Run-Time Verification Via Testers
Intelligent and Dependable Decision-Making Under Uncertainty
Model Integration and Cyber Physical Systems: A Semantics Perspective
A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking
A Formal Approach to Architectural Design Patterns
Towards Consistent Specifications of Product Families
Symbolic Computation in Automated Program Reasoning
PrideMM: Second Order Model Checking for Memory Consistency Models
The Value of Verification: Positive Experience of Industrial Proof
Development and Application of a Meta IV Compiler
csp2B: A Practical Approach to Combining CSP and B
Certifying Airport Security Regulations Using the Focal Environment
Parameterized Verification of Round-Based Distributed Algorithms via Extended Threshold Automata
Computing Meta-transitions for Linear Transition Systems with Polynomials
Concolic Testing Heap-Manipulating Programs
Controlling Object Allocation Using Creation Guards
A Survey of Papers from Formal Methods for Interactive Systems (FMIS) Workshops
Modelling Microsoft COM Using pi-Calculus
A Metric Encoding for Bounded Model Checking
Using a Logical and Categorical Approach for the Validation of Fault-Tolerant Systems
Enriching the Software Development Process by Formal Methods
Formal Specifications and Software Testing, a Fruitful Convergence
When Equivalence and Bisimulation Join Forces in Probabilistic Automata
A New System Engineering Methodology Coupling Formal Specification and Performance Evaluation
Description is our Business
A UNITY Mapping Operator for Distributed Programs
End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform
Towards an Integrated CASE and Theorem Proving Tool for VDM-SL
Combining the Design of Industrial Systems with Effective Verification Techniques
The META-Language: A Reference Manual
The Delft VDM-SL Front-End
Verifying Auto-generated C Code from Simulink - An Experience Report in the Automotive Domain
RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 Instructions
Mapping Statecharts to Verilog for Hardware/Software Co-specification
Improved BDD-Based Discrete Analysis of Timed Systems
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified
Applying Software Model Checking Techniques for Behavioral UML Models
The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem Theorems
The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification
Transacted Memory for Smart Cards
Experiences in Embedded Scheduling
Model-Based Problem Solving for University Timetable Validation and Improvement
Structured Formal Verification of a Fragment of the IBM S/390 Clock Chip
Robust Data Types
Formal Verification of Complex Data Paths: An Industrial Experience
Modularizing the Formal Description of a Database System
A Semantics for NewSpeak in VDM-SL
Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I
Group Principals and the Formalization of Anonymity
A Map of Asynchronous Communication Models
Specification with Class: A Brief History of Object-Z
Learning Moore Machines from Input-Output Traces
An EVES Data Abstraction Example
1st Workshop on Uses of Symbolic Execution, USE@FM 2015, Oslo, Norway, June 23-25, 2015
A Metalanguage for the Formal Requirement Specification of Reactive Systems
Formal Methods in the Security Business: Exotic Flowers Thriving in an Expanding Niche
Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study
Trace Abstraction-Based Verification for Uninterpreted Programs
System Verification through Program Verification
Specifying a Safety-Critical Control System in Z
Symbolic Model Checking with Fewer Fixpoint Computations
Fast Attack Graph Defense Localization via Bisimulation
Knowledge-Based Automated Repair of Authentication Protocols
Hierarchical Specification of Abstract Data Types
Apply Formal Methods in Certifying the SyberX High-Assurance Kernel
Visual Verification of Safety and Liveness
The Formal Definition of Modula-2 and Its Associated Interpreter
The RAISE Language, Method and Tools
Identification of and Solutions to Shortcomings of LCL, a Larch/C Interface Specification Language
Stochastic Games for User Journeys
A Decision Diagram Operation for Reachability
Compiling C and C++ Programs for Dynamic White-Box Analysis