yusuke1997/dblp-id-title huggingface dataset:
Concept Use or Concept Refinement: An Important Distinction in Building Generic Specifications
Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks
Formal Derivation of a Distributed Program in Event B
Correct Channel Passing by Construction
Conformance Testing Based on UML State Machines
Detecting Deadlock in Ada Rendezvous Flow Structure Based on Process Algebra
The Semantics and Tool Support of OZTA
RAFFS: Model Checking a Robust Abstract Flash File Store
Four-Valued Monitorability of ømega-Regular Languages
Deriving Probabilistic Semantics Via the 'Weakest Completion'
Specifying and Verifying Sensor Networks: An Experiment of Formal Methods
Complete Model-Based Equivalence Class Testing for the ETCS Ceiling Speed Monitor
Time Aware Modelling and Analysis of Multiclocked VLSI Systems
Formal Kinematic Analysis of Epicyclic Bevel Gear Trains
Mechanization of an Integrated Approach: Shallow Embedding into SAL/PVS
On the Formal Analysis of HMM Using Theorem Proving
Parallel Chopped Symbolic Execution
3rd IEEE International Conference on Formal Engineering Methods, ICFEM 2000, York, England, UK, September 4-7, 2000, Proceedings
Contextual Trace Refinement for Concurrent Objects: Safety and Progress
Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking
Learning Mealy Machines with Local Timers
Maintaining Referential Integrity on the Web
Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols co-located with the 23rd International Conference on Formal Engineering Methods (ICFEM 2022), Madrid, Spain, October 24, 2022
A Model-to-Implementation Mapping Tool for Automated Model-Based GUI Testing
On Clock Difference Constraints and Termination in Reachability Analysis of Timed Automata
Tool for Translating Simulink Models into Input Language of a Model Checker
Circular Coinduction with Special Contexts
Comparison of Model Checking Tools for Information Systems
Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems
A Resource-Based Logic for Termination and Non-termination Proofs
Engineering Quality Software
DFTCalc: Reliability Centered Maintenance via Fault Tree Analysis (Tool Paper)
Towards Dependable and Explainable Machine Learning Using Automated Reasoning
Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks
Towards a Model Checker for NesC and Wireless Sensor Networks
Stateful Dynamic Partial-Order Reduction
Modal Characterisations of Probabilistic and Fuzzy Bisimulations
A Practical Approach to Partiality - A Proof Based Approach
Timed Automata Verification via IC3 with Zones
Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis
Incremental Property Directed Reachability
Faster Analysis of Formal Specifications
Ubiquitous Abstraction: A New Approach to Mechanized Formal Verification
On Probabilistic Extension of the Interaction Theory
Loop Invariant Synthesis in a Combined Domain
Enhanced Semantic Access to Formal Software Models
An Algebra of Quantum Programs with the Kleene Star Operator
Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction
Fast Translation from LTL to Büchi Automata via Non-transition-based Automata
An Evidential Tool Bus
A Mathematical Framework for Safecharts
Verification of ATL Transformations Using Transformation Models and Model Finders
Formalization, Testing and Execution of a Use Case Diagram
Testing for Refinement in CSP
Offering Formal Verification Capabilities for Industry Standard Case Tools: Challenges and Results
Equational Abstraction Refinement for Certified Tree Regular Model Checking
The Description of CORBA Objects Based on Petri Nets
Robustness and Failure Detection in Epistemic Gossip Protocols
An Overview of Mobile Object-Z
Invited talk: Formal Verification of Quantum Protocols
Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude
Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing
A Theory of Secure Control Flow
Consistency Verification of Specification Rules
A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented Paradigm
Generic Engineering of Communication Protocols - Current Experience and Future Issues
Quantitative Program Dependence Graphs
Refinement-Preserving Co-evolution
A Compositional Framework for Service Interaction Patterns and Interaction Flows
Using PVS to Prove Properties of Systems Modelled in a Synchronous Dataflow Language
A General Lattice Model for Merging Symbolic Execution Branches
A Methodological Approach to the Requirement Specification of Embedded Systems
CASTING: A Formally Based Software Test Generation Method
Generation of a Reversible Semantics for Erlang in Maude
Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude
Constraint-Based Model Checking of Data-Independent Systems
Using Transition Systems to Unify UML Models
An Improved Rule for While Loops in Deductive Program Verification
Frameworks in Catalysis: Pictorial Notation and Formal Semantics
Differencing Labeled Transition Systems
Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System
Formalizing Process Scheduling Requirements for an Aircraft Operational Flight Program
Reconstructing Paths for Reachable Code
Formal Reasoning about Hardware and Software Memory Models
Formally Verified Trades in Financial Markets
Software Measurement and Formal Methods: A Case Study Centered on TRIO+ Specifications
Certifying Hardware Model Checking Results
Refinement-Based Modelling and Verification of Design Patterns for Self-adaptive Systems
Laws of Pattern Composition
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties
Checking Activity Transition Systems with Back Transitions Against Assertions
A Concurrent Temporal Programming Model with Atomic Blocks
Analysis on Strategies of Superposition Refinement of Event-B Specifications
BCCIC3: Batch Clause Construction Enhanced Generalization in IC3
PDNet: A Programming Language for Software-Defined Networks with VLAN
Reasoning about Programs Using a Scientific Method
Formalising an Integrated Language in PVS
A Flexible Approach for Finding Optimal Paths with Minimal Conflicts
A Calculus for Mobile Network Systems
A 3-Valued Contraction Model Checking Game: Deciding on the World of Partial Information
More Anti-chain Based Refinement Checking
The Use of Mathematics in Software Engineering
A Formal Metamodeling Approach to a Transformation between the UML State Machine and Object-Z
Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP
Using Use Cases in Executable Z
A Formal Definition of Function Points for Automated Measurement of B Specifications
Toward Practical Application of Formal Methods in Software Lifecycle Processes
Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior
The Continuum Hypothesis Implies the Existence of Non-principal Arithmetical Ultrafilters - A Coq Formal Verification
Modelling and Proof of a Tree-Structured File System in Event-B and Rodin
Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings
A Verification Framework for Agent Knowledge
Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry
Tutorial on the RAISE Language, Method and Tools
Architectural Verification of Control Systems Using CSP
Clock-Dependent Probabilistic Timed Automata with One Clock and No Memory
Learning Types for Binaries
Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings
A Formal Engineering Approach to High-Level Design of Situation Analysis Decision Support Systems
The Circus Testing Theory Revisited in Isabelle/HOL
User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition
A Verification System for Distributed Objects with Asynchronous Method Calls
Quantitative Analysis of Information Flow Using Theorem Proving
Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code
Research on Ontology-Oriented Domain Analysis on MIS
Reasoning about Liveness Properties in Event-B
A Refinement Tool for Z
Verifying chi Models of Industrial Systems with Spin
Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool
Heuristic-Guided Abstraction Refinement for Concurrent Systems
Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings
Model Checking in Practice: Analysis of Generic Bootloader Using SPIN
Dynamic Extrapolation in Extended Timed Automata
Mapping RT-LOTOS Specifications into Time Petri Nets
Interactive Verification of UML State Machines
A Sliding-Window Algorithm for On-The-Fly Interprocedural Program Analysis
Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems
Simple LTL Model Checking on Finite and Infinite Traces over Concrete Domains
When Can Formal Methods Make a Real Difference?
A Relational Model for Formal Object-Oriented Requirement Analysis in UML
Formal Verification of Programs Computing the Floating-Point Average
Design of Point-and-Click User Interfaces for Proof Assistants
Practical Analysis Framework for Component Systems with Dynamic Reconfigurations
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators
A Runtime Verification Framework for Cyber-Physical Systems Based on Data Analytics and LTL Formula Learning
A Knowledge-Based Verification Method for Dynamic Access Control Policies
Structuring Reactive Systems in B AMN
A Calculus for Set-Based Program Development
Modelling and Refinement of an On-Chip Communication Architecture
Formally Verified Animation for RoboChart Using Interaction Trees
Incremental Slicing
Formal Modeling and Analysis of Cassandra in Maude
The Specification-Based Testing of a Trusted Kernel: MK++
Formal Representation and Analysis of Batch Stock Trading Systems by Logical Petri Net Workflows
Discovering Likely Method Specifications
A First Step in the Translation of Alloy to Coq
Abstract Program Slicing: From Theory towards an Implementation
Proving Event-B Models with Reusable Generic Lemmas
Specification-Based Class Testing: A Case Study
A Formal Descriptive Semantics of UML
Finding Bugs in Network Protocols Using Simulation Code and Protocol-Specific Heuristics
Fragmented Retrenchment, Concurrency and Fairness
Multi-threaded On-the-Fly Model Generation of Malware with Hash Compaction
Improving Probability Estimation Through Active Probabilistic Model Learning
Verifying Nested Lock Priority Inheritance in RTEMS with Java Pathfinder
A Reversible Operational Semantics for Imperative Programming Languages
Making the Right Cut in Model Checking Data-Intensive Timed Systems
Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings
Integration of Metamorphic Testing with Program Repair Methods Based on Adaptive Search Strategies and Program Equivalence
A UTP Semantics for Communicating Processes with Shared Variables
Maximally Abstract Retrenchments
Efficient Path Finding with the Sweep-Line Method Using External Storage
Formal Methods and Software Engineering, 7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, UK, November 1-4, 2005, Proceedings
Security Analysis of Smart Home Implementations
Engineering a Theory of Concurrent Programming
A Framework for Multi-view Reconciliation and for Medical Devices Personalization
An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres
Mechanical Verification of Transaction Processing Systems
Automatic Extraction of Object-Oriented Observer Abstractions from Unit-Test Executions
Formal Verification of a Memory Model for C -Like Imperative Languages
Towards Abstraction for DynAlloy Specifications
Symbolic Verification of Distributed Real-Time Systems with Complex Synchronizations
Unifying Theories of Parallel Programming
Policy Dependent and Independent Information Flow Analyses
Modular Analysis of Tree-Topology Models
Development of Security Software: A High Assurance Methodology
Refinement of Information Flow Architectures
Testing Real-Time Multi Input-Output Systems
Verification of Orchestration Systems Using Compositional Partial Order Reduction
Model-Based Specification Animation Using Testgraphs
Adding Formalism to Methods or Where and When Will Industry Use Formal Reasoning?
Controller Synthesis for Object Petri Nets
Formalizing the Transaction Flow Process of Hyperledger Fabric
Modeling and Analysis of Thread-Pools in an Industrial Communication Platform
Specification-Based Test Generation for Security-Critical Systems Using Mutations
Specification and Analysis of System Level Inter-Component Communication
A Certified Decision Procedure for Tree Shares
Verifying Heap-Manipulating Programs with Unknown Procedure Calls
The Equivalence of Statecharts
The Common Semantic Constructs of XML Family
A Unified Algebraic Framework for Specifying Communication Protocols
Tutorial: Software Model Checking
From Requirements to Development: Methodology and Example
A CEGAR Scheme for Information Flow Analysis
Graph Convolutional Network Robustness Verification Algorithm Based on Dual Approximation
Combining Deep Learning and Probabilistic Model Checking in Sports Analytics
SALT - Structured Assertion Language for Temporal Logic
Formal Specification and Verification of Smart Contracts
Vulnerability Detection via Typestate-Guided Code Representation Learning
Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings
Complementary Methodologies for Developing Hybrid Systems with Event-B
Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings
Enhanced Distributed Behavioral Cartography of Parametric Timed Automata
Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking
Model Based Testing of Cyber-Physical Systems
Application of Embedded Testing Methods to Service Validation
On Concept-Based Definition of Domain-Specific Languages
Specification of an Asynchronous On-chip Bus
A Specification-Based Software Construction Framework for Reuse
Proving Inductive Theorems Using Witnessed Test Sets
Managing Verification Activities Using SVM
Multi-prover Verification of C Programs
Refinement-Based Verification of the FreeRTOS Scheduler in VCC
Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications
The Miles Before Formal Methods - A Case Study on Modeling and Analyzing a Passenger Lift System
Formal Verification of the Heap Manager of an Operating System Using Separation Logic
The Domain of Parametric Hypercubes for Static Analysis of Computer Games Software
Reducing Model Checking of the Few to the One
Continuation Semantics for Concurrency with Multiple Channels Communication
Automating Coinduction with Case Analysis
Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS
Machine-Checked Executable Semantics of Stateflow
Verifying Temporal Properties of C Programs via Lazy Abstraction
CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions
Automatic Verification for Node-Based Visual Script Notation Using Model Checking
Multi-process Systems Analysis Using Event B: Application to Group Communication Systems
Integrating Formal Methods with System Management
Distributed Theorem Proving for Distributed Hybrid Systems
Machine-Assisted Proof Support for Validation Beyond Simulink
Issues in Implementing a Model Checker for Z
A Reasoning Method for Timed CSP Based on Constraint Solving
Adaptive Random Testing by Bisection with Restriction
Program Verification Through Computer Algebra
Formal Development of a Distributed Logging Mechanism Supporting Disconnected Updates
A System Substitution Mechanism for Hybrid Systems in Event-B
Formal Methods and Software Engineering, 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007, Proceedings
Three Perspectives in Formal Engineering
Programmers Ain't Mathematicians, and Neither Are Testers
Modal Systems: Specification, Refinement and Realisation
Slicing Hierarchical Automata for Model Checking UML Statecharts
Efficient Symbolic Execution of Large Quantifications in a Process Algebra
Assume-Guarantee Reasoning with Local Specifications
Accurate Abstractions for Controller Synthesis with Non-uniform Disturbances
Conformance Checking of Dynamic Access Control Policies
Bounded Model Checking High Level Petri Nets in PIPE+Verifier
Proof Assisted Model Checking for B
Formal Specification of Evolutionary Software Agents
B Model Animation for External Verification
Asynchronous Communication in MSVL
SMTBCF: Efficient Backbone Computing for SMT Formulas
Formal Derivation of Multilayered Hardware/Software Structures
Combining Parallel Emptiness Checks with Partial Order Reductions
vTRUST: A Formal Modeling and Verification Framework for Virtualization Systems
Managing Complexity through Abstraction: A Refinement-Based Approach to Formalize Instruction Set Architectures
Towards Verifying Ethereum Smart Contracts at Intermediate Language Level
A Formal Model for the Block Device Subsystem of the Linux Kernel
Realising the Benefits of Formal Methods
Second IEEE International Conference on Formal Engineering Methods, ICFEM 1998, Brisbane, Queensland, Australia, December 9-11, 1998, Proceedings
Verification of Computation Orchestration Via Timed Automata
Robustness of Piece-Wise Linear Neural Network with Feasible Region Approaches
Probably Approximate Safety Verification of Hybrid Dynamical Systems
A General Model for Reachability Testing of Concurrent Programs
Formalizing UML Models with Object-Z
Mining Dataflow Sensitive Specifications
Strongly Typed Numerical Computations
An Operational Semantics for ZCCS
Separation Predicates: A Taste of Separation Logic in First-Order Logic
Validation of Security-Design Models Using Z
Selective Integration of Formal Methods in the Development of Electronic Control Units
Formal Analysis of Power Electronic Systems
SqlSol: An accurate SQL Query Synthesizer
Formal Foundations of Object-Oriented Modeling Notations
A Semantic Model for Service Composition with Coordination Time Delays
Formalization and Verification of Declarative Cloud Orchestration
Simulations for Multi-Agent Systems with Imperfect Information
Approximate Model Checking of PCTL Involving Unbounded Path Properties
CASSANDRA: An Online Failure Prediction Strategy for Dynamically Evolving Systems
From a B Specification to UML StateChart Diagrams
Specification Translation of State Machines from Equational Theories into Rewrite Theories
Formal Automatic Verification of Authentication Crytographic Protocols
Counterexample Guided Abstraction Refinement Via Program Execution
A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces
Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languages
Delta-Oriented FSM-Based Testing
Concolic Unbounded-Thread Reachability via Loop Summaries
Towards a Formal Verification Methodology for Collective Robotic Systems
Domain-Specific Languages with Scala
A Representative Function Approach to Symmetry Exploitation for CSP Refinement Checking
Towards Dynamically Communicating Abstract Machines in the B Method
Towards the Semantics for Web Service Choreography Description Language
CDGDroid: Android Malware Detection Based on Deep Learning Using CFG and DFG
Inconsistency Analysis of Time-Based Security Policy and Firewall Policy
Theorem Proving for Maude Specifications Using Lean
A Deterministic Interpreter Simulating a Distributed Real Time System Using VDM
Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks
Interaction Interfaces - Towards a Scientific Foundation of a Methodological Usage of Message Sequence Charts
PRTS: An Approach for Model Checking Probabilistic Real-Time Hierarchical Systems
Model Checking Dynamic UML Consistency
Domain-Driven Probabilistic Analysis of Programmable Logic Controllers
Sweep-Line Analysis of TCP Connection Management
TTT/ik: Learning Accurate Mealy Automata Efficiently with an Imprecise Symbol Filter
Improving Automatic Verification of Security Protocols with XOR
A New Algorithm for Service Interaction Detection
A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators
Towards a Refinement Calculus for Concurrent Real-Time Programs
SCC-Based Improved Reachability Analysis for Markov Decision Processes
Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq
Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages
An Approach to Preserve Protocol Consistency and Executability Across Updates
Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices
Modelling Real-Time Systems with Continuous-Time Temporal Logic
LLM-SYM: Integrating Symbolic Methods and Large Language Models for Automated Theorem Proving
An AMBA-ARM7 Formal Verification Platform
Proceedings of the First International Workshop on Formal Methods for Interactive Systems, FMIS@ICFEM 2006, Macao, October 31, 2006
Bounded Semantics of CTL and SAT-Based Verification
Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings
Defining Differentiation and Integration in Z
SysML Blocks Adaptation
SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol
NL2CTL: Automatic Generation of Formal Requirements Specifications via Large Language Models
The Formal Specification of the Fieldbus Foundation Link Scheduler in E-LOTOS
Timed Patterns: TCOZ to Timed Automata
A Relational Static Semantics for Call Graph Construction
An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems
Conditions for Avoiding Controllability Problems in Distributed Testing
A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs
Formal Analysis of FreeRTOS Scheduler on ARM Cortex-M4 Cores
Decomposition for Compositional Verification
Machine-Checked Sequencer for Critical Embedded Code Generator
Towards Certified Runtime Verification
Michael Jackson's Problem Frames: Towards Methodological Principles of Selecting and Applying Formal Software Development Techniques and Tools
Engineering Software for Modular Formalisation and Verification of STV Algorithms
A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata
Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language
A Formal Verification Study on the Rotterdam Storm Surge Barrier
Using CARE to Construct Verified Software
ABC/ADL: An ADL Supporting Component Composition
A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams
Formalizing Robustness Against Character-Level Perturbations for Neural Network Language Models
API Conformance Verification for Java Programs
Verifying Neural Networks by Approximating Convex Hulls
A Knowledge Based Analysis of Cache Coherence
Systematic Formal Verification of Interpreters
Automatic Synthesis of Controllers from Formal Specifications
Towards Building a Generic Vulnerability Detection Platform by Combining Scalable Attacking Surface Analysis and Directed Fuzzing
Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006, Proceedings
An Empirical Study of Structural Constraint Solving Techniques