yusuke1997/dblp-id-title huggingface dataset:
SMT-Based Analysis of Biological Computation
Deductive Model Refinement
NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16-18, 2023, Proceedings
More Automated Formal Methods?! If so, why, where & how?
Practical Causal Models for Cyber-Physical Systems
SimCheck: An Expressive Type System for Simulink
A Modular Way to Reason About Iteration
Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif
Configurable Benchmarks for C Model Checkers
Verification of Numerical Programs: From Real Numbers to Floating Point Numbers
Experience Report: Application of Falsification Methods on the UxAS System
Online Shielding for Stochastic Systems
Strategy Synthesis for Autonomous Agents Using PRISM
Towards Co-Engineering Communicating Autonomous Cyber-physical Systems
Slicing AADL Specifications for Model Checking
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms
Model Checking - My 27-year Quest to Overcome the State Explosion Problem
HyTwin: Hybrid Program Semantics for Digital Twin-Based Security Interventions in Industrial Control Systems
Blocked Literals Are Universal
Reasoning About Safety-Critical Information Flow Between Pilot and Computer
From Retrospective Verification to Forward-Looking Development
From Verified Scala to STIX File System Embedded Code Using Stainless
Verifying Attention Robustness of Deep Neural Networks Against Semantic Perturbations
Generating Data Race Witnesses by an SMT-Based Analysis
Mode-Based Reactive Synthesis
Approximate Translation from Floating-Point to Real-Interval Arithmetic
On-the-Fly Model Checking with Neural MCTS
Designing a Deadlock-Free Train Scheduler: A Model Checking Approach
An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data
Model-Checking Task Parallel Programs for Data-Race
Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B
CLSE: Closed-Loop Symbolic Execution
A Formal Proof of the Lax Equivalence Theorem for Finite Difference Schemes
Rewrite-Based Decomposition of Signal Temporal Logic Specifications
Data Model Bugs
Integrating Runtime Verification into a Sounding Rocket Control System
MoDeS3: Model-Based Demonstrator for Smart and Safe Cyber-Physical Systems
Practical Partial Order Reduction for CSP
Verification of LSTM Neural Networks with Non-linear Activation Functions
Combining PVSio with Stateflow
Scalable Reliability Analysis by Lazy Verification
A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios
Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction
Distinguishing Sequences for Partially Specified FSMs
Verified Probabilistic Policies for Deep Reinforcement Learning
A Prototype Embedding of Bluespec SystemVerilog in the PVS Theorem Prover
Verifying Min-Plus Computations with Coq
Modeling Guidelines for Code Generation in the Railway Signaling Context
Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol
Extending Dynamic Logics with First-Class Relational Reasoning
Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT
Enclosing Temporal Evolution of Dynamical Systems Using Numerical Methods
Verification of an Anti-unification Algorithm in PVS
Topllet: An Optimized Engine for Answering Metric Temporal Conjunctive Queries
Design and Runtime Verification Side-by-Side in eTrice
Symbolic Computation of Strongly Connected Components Using Saturation
Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning
Data Independence for Software Transactional Memory
Leadership Election: An Industrial SoS Application of Compositional Deadlock Verification
Constraint Caching Revisited
OnTrack: An Open Tooling Environment for Railway Verification
Model Construction and Priority Synthesis for Simple Interaction Systems
Using PVS to Investigate Incidents through the Lens of Distributed Cognition
Verifying a Class of Certifying Distributed Programs
Call Invariants
Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems
Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants
jUnit RV -Adding Runtime Verification to jUnit
Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation
OpenJML: JML for Java 7 by Extending OpenJDK
HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis
Belief Bisimulation for Hidden Markov Models - Logical Characterisation and Decision Algorithm
Generalizing a Mathematical Analysis Library in Isabelle/HOL
Detecting MPI Zero Buffer Incompatibility by SMT Encoding
Automata Size Reduction by Procedure Finding
Testing-Based Compiler Validation for Synchronous Languages
Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft
Verification of Functional Correctness of Code Diversification Techniques
Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness
NASA Formal Methods - 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings
The Measurement Library: Representing Physical Types in PVS
nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement
Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software
Output Range Analysis for Deep Feedforward Neural Networks
Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines
NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings
Recursive Variable-Length State Compression for Multi-core Software Model Checking
Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq
Formal Verification of Large Software Systems
Statistical Model Checking of Ad Hoc Routing Protocols in Lossy Grid Networks
Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints
Automated Testcase Generation for Numerical Support Functions in Embedded Systems
Quantitative Verification and Strategy Synthesis for BDI Agents
Incremental Transitive Closure for Zonal Abstract Domain
Mechanized Semantics for Correctness of the RS274 Additive Manufacturing Command Language
Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations
NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings
Neural Network Compression of ACAS Xu Early Prototype Is Unsafe: Closed-Loop Verification Through Quantized State Backreachability
Extending the GWV Security Policy and Its Modular Application to a Separation Kernel
Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework
Eliminating Flakiness: Deterministic Control for Validating Nondeterministic Asmeta Specifications
Quasi-Equal Clock Reduction On-the-Fly
Automated Requirements-Based Testing of Black-Box Reactive Systems
The Prusti Project: Formal Verification for Rust
On Symmetry and Quantification: A New Approach to Verify Distributed Protocols
Timely Rollback: Specification and Verification
Modular Model-Checking of a Byzantine Fault-Tolerant Protocol
A Relational Shape Abstract Domain
BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software
EventB2Java: A Code Generator for Event-B
A Mixed Real and Floating-Point Solver
Synthesizing Runtime Enforcer of Safety Properties Under Burst Error
Using Model-Checking to Reveal a Vulnerability of Tamper-Evident Pairing
Local Reasoning for Parameterized First Order Protocols
Shape Analysis with Connectors
Optimal Storage of Combinatorial State Spaces
Compositional Runtime Enforcement
Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty
Online Parametric Timed Pattern Matching with Automata-Based Skipping
A Formal Verification Framework for Runtime Assurance
SpeAR v2.0: Formalized Past LTL Specification and Analysis of Requirements
A Machine-Checked Proof of A State-Space Construction Algorithm
NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings
A Linear Weight Transfer Rule for Local Search
Structured Synthesis for Probabilistic Systems
Heterogeneous Verification of an Autonomous Curiosity Rover
Formal Verification of Composite Field Multipliers for Information-Theoretically Secure Radio Communication in Spacecraft Control
The OpenTheory Standard Theory Library
Adiar 1.1 - Zero-Suppressed Decision Diagrams in External Memory
Automated Backend Selection for ProB Using Deep Learning
On Conflict-Driven Reasoning
On the Effectiveness of Signal Rescaling in Hybrid System Falsification
Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory
On the Quantum Formalization of Coherent Light in HOL
Theorem Proving in Intel Hardware Design
Automating Program Transformation with Coccinelle
Inferring Automata with State-Local Alphabet Abstractions
A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Select
Verified ROS-Based Deployment of Platform-Independent Control Systems
SMT-Based Aircraft Conflict Detection and Resolution
Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty
Asynchronous Composition of Local Interface LTL Properties
NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings
Just Formal Enough? Automated Analysis of EARS Requirements
Multi-objective Task Assignment and Multiagent Planning with Hybrid GPU-CPU Acceleration
NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings
TRACE: Toolkit for Requirements Analysis, Capture, and Elicitation
Mechanized, Compositional Verification of Low-Level Code
Efficient Verification of Optimized Code - Correct High-Speed X25519
Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application
Using Language Engineering to Lift Languages and Analyses at the Domain Level
Reachability Analysis Using Extremal Rates
Approximate Conformance Verification of Deep Neural Networks
Abstract Model Repair
Semantics for Locking Specifications
From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent Systems
Program Sketching Using Lifted Analysis for Numerical Program Families
Compact Proof Witnesses
Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems đagger
Compositional Falsification of Cyber-Physical Systems with Machine Learning Components
Learning-Based Testing of an Industrial Measurement Device
Systematic Predicate Abstraction Using Variable Roles
Parameter Synthesis and Robustness Analysis of Rule-Based Models
SMT-Based Model Checking
Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust
Improved Learning for Stochastic Timed Models by State-Merging Algorithms
Scaling Up with Event-B: A Case Study
Stubborn Transaction Reduction
Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids
Stochastic Formal Methods for Hybrid Systems
Automatic Generation of DO-178 Test Procedures
An Infrastructure for Faithful Execution of Remote Attestation Protocols
Generating Verifiable Java Code from Verified PVS Specifications
Contract-Driven Runtime Adaptation
Parametric Model Checking Timed Automata Under Non-Zenoness Assumption
DSV: Disassembly Soundness Validation Without Assuming a Ground Truth
An SMT Formalization of Mixed-Precision Matrix Multiplication - Modeling Three Generations of Tensor Cores
A Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing
Hierarchical Safety Cases
Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study
Verification of Fault-Tolerant Protocols with Sally
The MINERVA Software Development Process
Formal Stability Analysis of Optical Resonators
Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations
A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata
Asm2C++: A Tool for Code Generation from Abstract State Machines to Arduino
Compositional Verification of Architectural Models
Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification
Event-B at Work: Some Lessons Learnt from an Application to a Robot Anti-collision Function
On Proving Recoverability of Smart Electrical Grids
Class-Modular, Class-Escape and Points-to Analysis for Object-Oriented Languages
Automatically Detecting Inconsistencies in Program Specifications
Runtime Verification Triggers Real-Time, Autonomous Fault Recovery on the CySat-I
Verifying Nonpolynomial Hybrid Systems by Qualitative Abstraction and Automated Theorem Proving
Real Arithmetic in TLAPM
A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
Qualification of a Model Checker for Avionics Software Verification
Verification of Faulty Message Passing Systems with Continuous State Space in PVS
specgen: A Tool for Modeling Statecharts in CSP
Formal Validation and Verification Framework for Model-Based and Adaptive Control Systems
Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL Properties
Checking and Distributing Statistical Model Checking
Reward Shaping from Hybrid Systems Models in Reinforcement Learning
Multi-timed Bisimulation for Distributed Timed Automata
Strengthening Deterministic Policies for POMDPs
Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs
Permutation Invariance of Deep Neural Networks with ReLUs
Compositional Verification of Parameterised Timed Systems
On Designing an ACL2-Based C Integer Type Safety Checking Tool
Towards Complete Specifications with an Error Calculus
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C
First NASA Formal Methods Symposium - NFM 2009, Moffett Field, California, USA, April 6-8, 2009
Approximate Quantifier Elimination for Propositional Boolean Formulae
Fly-by-Logic: A Tool for Unmanned Aircraft System Fleet Planning Using Temporal Logic
A Benchmark Suite for Hybrid Systems Reachability Analysis
Distributional Probabilistic Model Checking
Model-Counting Approaches for Nonlinear Numerical Constraints
Hypercontracts
On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols
A Toolkit for Automated Testing of Dafny
Specification Decomposition for Reactive Synthesis
Freshness and Reactivity Analysis in Globally Asynchronous Locally Time-Triggered Systems
A Safety Case Pattern for Model-Based Development Approach
Sum of Abstract Domains
From Passive to Active: Learning Timed Automata Efficiently
Static Value Analysis of Python Programs by Abstract Interpretation
Automated Formal Verification of the TTEthernet Synchronization Quality
Distributed Model Checking Using ProB
On Implementing Real-Time Specification Patterns Using Observers
Specification and Proof of High-Level Functional Properties of Bit-Level Programs
Coloured Petri net refinement specification, and correctness proof with Coq
Partial Order Reduction and Symmetry with Multiple Representatives
Rare Event Simulation for Stochastic Hybrid Systems Using Symbolic Importance Functions
The Power of Disjoint Support Decompositions in Decision Diagrams
ML ν : A Distributed Real-Time Modal Logic
Improved on-the-Fly Livelock Detection
jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2
Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems
Using Standard Typing Algorithms Incrementally
Formal Assurance for Cooperative Intelligent Autonomous Agents
Formalizing CNF SAT Symmetry Breaking in PVS
On-the-Fly Confluence Detection for Statistical Model Checking
LiquidPi: Inferrable Dependent Session Types
Formal Verification of Parallel Prefix Sum
Generalized Abstract Symbolic Summaries for Differencing Heap-manipulating Programs
LLVM2CSP : Extracting CSP Models from Concurrent Programs
Runtime Verification Meets Android Security
Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry
Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution
Incremental Verification with Mode Variable Invariants in State Machines
Towards a Formal Safety Framework for Trajectories
Synthesis for PCTL in Parametric Markov Decision Processes
Algorithmic Analysis of Event-B in Rewriting Logic
Regular Model Checking Using Solver Technologies and Automata Learning
Integrating Formal Verification and Assurance: An Inspection Rover Case Study
The Gradual Verifier
DO-333 Certification Case Studies
NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings
Code Generation Using a Formal Model of Reference Counting
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis
hpnmg: A C++ Tool for Model Checking Hybrid Petri Nets with General Transitions
Developing Verified Software Using Leon
Verifying an Aircraft Collision Avoidance Neural Network with Marabou
Some Steps into Verification of Exact Real Arithmetic
Specification in PDL with Recursion
SPEN: A Solver for Separation Logic
Robust Computation Tree Logic
Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code
Towards a Two-Layer Framework for Verifying Autonomous Vehicles
Zone Extrapolations in Parametric Timed Automata
Modeling Regular Replacement for String Constraint Solving
Symbolic Model Checking of Weighted PCTL Using Dependency Graphs
Reachability Analysis for Cyber-Physical Systems: Are We There Yet?
Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior
Towards Realizability Checking of Contracts Using Theories
Widening as Abstract Domain
Building a Formal Model of a Human-interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering
Integrated Contract-Based Unit and System Testing for Component-Based Systems
A Semantic Analysis of Wireless Network Security Protocols
Can Regulatory Bodies Expect Efficient Help from Formal Methods?
Model Checking for Autonomic Systems Specified with ASSL
Quantification of Battery Depletion Risk Made Efficient
The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS
D-Finder 2: Towards Efficient Correctness of Incremental Design
A Greedy Approach for the Efficient Repair of Stochastic Models
Model Checking with Edge-valued Decision Diagrams
Integrating Statechart Components in Polyglot
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
The Use of Automated Theory Formation in Support of Hazard Analysis
Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL
Extracting and Optimizing Formally Verified Code for Systems Programming
Formal API Specification of the PikeOS Separation Kernel
Safe Planning Through Incremental Decomposition of Signal Temporal Logic Specifications
Optimizing a Verified SAT Solver
Optimizing Control Strategy Using Statistical Model Checking
A module language for typing by contracts
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations
PyNuSMV: NuSMV as a Python Library
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem
Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals
Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution
NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings
Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking
Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites
Formal Verification of kLIBC with the WP Frama-C Plug-in
Integrating an Automated Theorem Prover into Agda
Automatic Review of Abstract State Machines by Meta Property Verification
Incremental Verification of Compiler Optimizations
Hardware-independent Proofs of Numerical Programs
Symmetry for the Analysis of Dynamic Systems
Synthesis of Greedy Algorithms Using Dominance Relations
Improving an Industrial Test Generation Tool Using SMT Solver
Implementing Cryptographic Primitives in the Symbolic Model
A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes
Verifying a C Implementation of Derecho's Coordination Mechanism Using VST and Coq
Reusable Formal Verification of DAG-Based Consensus Protocols
Conflict-Directed Graph Coverage
Software Model Checking without Source Code
Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis
Formalizing Probabilistic Safety Claims
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
Learning Symbolic Timed Models from Concrete Timed Data
Input Space Partitioning to Enable Massively Parallel Proof
Tackling the Polarity Initialization Problem in SAT Solving Using a Genetic Algorithm
Transaction Protocol Verification with Labeled Synchronization Logic
A Compositional Monitoring Framework for Hard Real-Time Systems
Using Test Ranges to Improve Symbolic Execution
On Learning Sparse Boolean Formulae for Explaining AI Decisions
Reachability Preservation Based Parameter Synthesis for Timed Automata
Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes
Applying Formal Methods to NASA Projects: Transition from Research to Practice
Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model
Software Model Checking of ARINC-653 Flight Code with MCP
Falsification of Cyber-Physical Systems with Constrained Signal Spaces
Centralized Multi-agent Synthesis with Spatial Constraints via Mixed-Integer Quadratic Programming
Runtime Verification of Generalized Test Tables
From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif
Reporting Races in Dynamic Partial Order Reduction
Sound Formal Verification of Linux's USB BP Keyboard Driver
A Case Study in Verification of Embedded Network Software
Evaluating Human-Human Communication Protocols with Miscommunication Generation and Model Checking
Condition Synthesis Realizability via Constrained Horn Clauses
Slice-based Formal Specification Measures - Mapping Coupling and Cohesion Measures to Formal Z
Specification Quality Metrics Based on Mutation and Inductive Incremental Model Checking
UFIT: A Tool for Modeling Faults in UPPAAL Timed Automata
Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables
Multi-Core LTSmin: Marrying Modularity and Scalability
From Hazard Analysis to Hazard Mitigation Planning: The Automated Driving Case
Per-Location Simulation
Hierarchical Verification of Quantum Circuits
An Executable Formal Framework for Safety-Critical Human Multitasking
Machine-Checkable Timed CSP
BDDs Strike Back - Efficient Analysis of Static and Dynamic Fault Trees
On the Timed Analysis of Big-Data Applications
NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings
Extracting Hybrid Automata from Control Code
An Even Better Approach - Improving the B.A.T.M.A.N. Protocol Through Formal Modelling and Analysis
Bounded Lazy Initialization
Quantitative Input Usage Static Analysis
Verifying a Privacy CA Remote Attestation Protocol
Learning Markov Models for Stationary System Behaviors
First-Order Transitive Closure Axiomatization via Iterative Invariant Injections
Qed. Computing What Remains to Be Proved
Simulating Synthesized Automata from Decentralized Specifications in LTL
The Improvement for Performance of Inter-VTS Data Exchange Format Protocol in VTS System
Behavior Execution Method for a Robot Using an Online Development Approach
Smart Device Locking System Provides Handy and Improved Security
Peers-Based Location of Mobile Devices
Platform Design for Data Sharing
Exclusive Region Based Scheduling for MB-OFDM UWB Using Hidden Pilot Sequences
Virtual Agent Learning for NUI/NUX-Based Games
Building Recognition Guided by Wi-Fi Based Localization
A Database Design for Pre-ordering System Based on Prediction of Customer Arrival Time