yusuke1997/dblp-id-title huggingface dataset:
Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM
SL-COMP: competition of solvers for separation logic
A Workshop on Formal Methods Education: An Aggregation of Opinions
Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method
On adaptive experiments for nondeterministic finite state machines
Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems
Analyzing program behavior through active automata learning
User-assisted code query customization and optimization
Extended abstract dependency graphs
Using linear algebra in decomposition of Farkas interpolants
Computational challenges in bounded model checking
Reformulating regression test suite optimization using quantum annealing - an empirical study
Proof engineering in the large: formal verification of Pentium?4 floating-point divider
Alternating simulation and IOCO
IntraJ: an on-demand framework for intraprocedural Java code analysis
Tradeoff exploration between reliability, power consumption, and execution time for embedded systems - The TSH tricriteria scheduling heuristic
On piggyback runtime monitoring of object-oriented programs
Let's verify this with Why3
Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model
Downward pattern refinement for timed automata
Monitoring modulo theories
Formal verification and security analysis of MQTT-SN
Programming in FISh
Evaluation of a distributed explicit state space exploration algorithm with state reconstruction for RDMA networks
Formal analysis of an AUTOSAR-based basic software module
Parallel and distributed model checking in Eddy
DT-Stark: a tool for evaluating the effectiveness of digital twins through feedback and perturbations
Mapping the design-space of textual variability modeling languages: a refined analysis
A distributed algorithm for strong bisimulation reduction of state spaces
End-to-end development of product lines for web systems
A framework for superscalar microprocessor correctness statements
Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2017
Machine-learning abstractions for component-based self-optimizing systems
Revealing and repairing configuration inconsistencies in large-scale system software
Constraint-based deductive model checking
Formal modeling and validation of Stateflow diagrams
Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach
CoCo 2019: report on the eighth confluence competition
Approximate reduction of finite automata for high-speed network intrusion detection
The physics of software tools: SWOT analysis and vision
Verifying a quantitative relaxation of linearizability via refinement
Crawlability metrics for automated web testing
The Log Skeleton Visualizer in ProM 6.9
Deterministic state space exploration
Formal methods and tools for industrial critical systems
CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems
Exploiting traces in static program analysis: better model checking through printf{{\tt printf}}s
An automated testing experiment for layered embedded C code
A toolset for conformance testing against UML sequence diagrams based on event-driven colored Petri nets
FAST: acceleration from theory to practice
Scenario-based verification of uncertain parametric MDPs
Worst-case execution-time analysis for embedded real-time systems
VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance
Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B
CLPS-B - A constraint solver to animate a B specification
From high-level modeling toward efficient and trustworthy circuits
Symbolic analysis via semantic reinterpretation
Handling loops in bounded model checking of C programs via k-induction
Reproducibility and replication of research results
Abstraction and refinement of mathematical functions toward SMT-based test-case generation
AutoProof meets some verification challenges
Application of BDDs in Boolean matching techniques for formal logic combinational verification
Learning single and compound-protocol automata and checking behavioral equivalences
Verification of the Capability Exchange Signalling protocol
Publisher Correction: Algorithm selection for SMT
DFT modeling approach for operational risk assessment of railway infrastructure
An integrated specification and verification technique for highly concurrent data structures
Easing maintenance of academic static analyzers
A general model checking framework for various memory consistency models
Algebraic aggregation of random forests: towards explainability and rapid evaluation
Main issues in protocol testing
Formal methods and automated verification of critical systems
Swarm model checking on the GPU
Workflows for quantitative data analysis in the social sciences
ASAP: A Source Code Authorship Program
Executable Petri net models for the analysis of metabolic pathways
From parametric trace slicing to rule systems
From objects to services: toward a stepwise migration approach for Java applications
Modelling and simulating a Thai railway signalling system using Coloured Petri Nets
Dynamic testing via automata learning
Replicable theory
Verification of critical systems described in real-time TiMo
Formal modeling and analysis of ad hoc Zone Routing Protocol in Event-B
An extension of first-order LTL with rules with application to runtime verification
On methods and tools for rigorous system design
Preface of "Specification and Validation of Real Time and Embedded systems in UML"
RTAMT - Runtime Robustness Monitors with Application to CPS and Robotics
Modelling and statistical model checking of a microgrid
Properties of two's complement floating point notations
CoVeriTest: interleaving value and predicate analysis for test-case generation
Bounded phase analysis of message-passing programs
Slicing concurrent Java programs using Indus and Kaveri
DivSIM , an interactive simulator for LLVM bitcode
Decision-diagram-based techniques for bounded reachability checking of asynchronous systems
State of the art in program analysis
Modular state space exploration for timed petri nets
Improved usability and performance of SMT solvers for debugging specifications
Go2Pins: a framework for the LTL verification of Go programs (extended version)
Non-numerical weakly relational domains
Counting Petri net markings from reduction equations
Pattern-based abstraction for verifying secrecy in protocols
FTSyn: a framework for automatic synthesis of fault-tolerance
Büchi Store: an open repository of ω-automata
Generating online test oracles from temporal logic specifications
ADTLang: a programming language approach to attack defense trees
Model checking and abstract interpretation as building blocks of advanced program analysis techniques - Selected papers from TACAS 2009
A greedy particle swarm optimization (GPSO) algorithm for testing real-world smart card applications
Programming dynamic reconfigurable systems
Analyzing the Execution Architecture of Mobile Phone Software with Colored Petri Nets
Formal verification of fault tolerance in safety-critical reconfigurable modules
Guest editors' introduction: quantitative analysis of real-time embedded systems
An approach for experimentally evaluating effectiveness and efficiency of coverage criteria for software testing
Template-based program verification and program synthesis
Generating effective tests for concurrent programs via AI automated planning techniques
Model checking of state-rich formalism Circus by linking to CSP ‖ B
Properties of state spaces and their applications
AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic
Statistical model checking: challenges and perspectives
Practical CTL * Model Checking: Should SPIN be Extended?
Runtime verification of concurrency-specific correctness criteria
Assessing SMT and CLP approaches for workflow nets verification
Distributed reachability analysis in timed automata
Proving the shalls
Multi-core symbolic bisimulation minimisation
Formal and experimental validation approaches in HCI systems design based on a shared event B model
Behavior-based model construction
Iterative delta debugging
Lightweight coarse-grained coordination: a scalable system-level approach
Sequential and distributed model checking of Petri nets
Flexibility in modeling languages and tools: a call to arms
Model-based software quality assurance tools and techniques presented at FASE 2018
A compositional framework for algebraic quantitative online monitoring over continuous-time signals
Interactive abstract interpretation: reanalyzing multithreaded C programs for cheap
prialt in Handel-C: an operational semantics
Modelling defence logistics networks
Probabilistic reachability for parametric Markov models
Special section on Coloured Petri Nets
Scalable and precise estimation and debugging of the worst-case execution time for analysis-friendly processors: a comeback of model checking
Analysis of recurrent neural networks via property-directed verification of surrogate models
Tool Support for Estimating the Memory Usage of Mobile Phone Software
Analyzing execution traces: critical-path analysis and distance analysis
Software verification challenges in the blockchain ecosystem
Model-checking fair dense-time systems with propositions and events
Automated formal analysis of temporal properties of Ladder programs
Architecture exploration and timing estimation during early design phases
New results in software model checking and analysis
Selected dynamic issues in software model checking
An IMS Performance Benchmark Implementation based on the TTCN-3 Language
From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata
Scientific workflows
Counter-example generation in symbolic abstract model-checking
Modelling and analysing a distributed dynamic channel allocation algorithm for mobile computing using high-level net methods
Introduction of TTCN-3 into the product development process: considerations from an electronic devices developer point of view
TOOLympics I: Competition on software testing
Formal Methods for Industrial Critical Systems
Environment-driven reachability for timed systems - Safety verification of an aircraft landing gear system
Evaluating workloads using comparative functional coverage
Efficient model-checking of weighted CTL with upper-bound constraints
Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture
Verification and validation meet planning and scheduling
Towards a "Synchronous Reactive" UML profile?
Discrete and continuous strategies for timed-arc Petri net games
Formal testing of timed graph transformation systems using metric temporal graph logic
An approach to quality engineering of TTCN-3 test specifications
Learning-based coordination model for spontaneous self-composition of reliable services in a distributed system
Verification of arithmetic circuits using binary moment diagrams
Validating timed UML models by simulation and verification
A decision procedure for detecting atomicity violations for communicating processes with locks
Integration of informal and formal development of object-oriented safety-critical software
A causal, time-independent synchronization pattern for collective adaptive systems
An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space
Fate and free will in error traces
Automation and intelligent scheduling of distributed system functional testing - Model-based functional testing in practice
Verifying safety of synchronous fault-tolerant algorithms by bounded model checking
Relating software validation to technology trends
TGV: theory, principles and algorithms
Verifiable strategy synthesis for multiple autonomous agents: a scalable approach
A uniform approach to three-valued semantics for μ -calculus on abstractions of hybrid automata
Reproducible and hackable software benchmarking with(out) compute clusters
Expressive program verification via structured specifications
A unified view of parameterized verification of abstract models of broadcast communication
Flush: an example of development by refinements in SCADE/Lustre
Comparing mutation coverage against branch coverage in an industrial setting
A blueprint for system-level performance modeling of software-intensive embedded systems
Constructive model-based analysis for safety assessment
Formal change impact analyses for emulated control software
Verifying OpenJDK's LinkedList using KeY (extended paper)
Tailored generation of concurrent benchmarks
Parameterized verification
Evaluating the effect of a lightweight formal technique in industry
Leveraging static analysis for cost-aware serverless scheduling policies
Slicing from formal semantics: Chisel - a tool for generic program slicing
Learning of behavioural models and dependency graphs for communicating systems with CkTailv2
A formal approach to AADL model-based software engineering
Paul Feyerabend and Software Technology
Formally verifying decompositions of stochastic specifications
Thoughtful brute-force attack of the RERS 2012 and 2013 Challenges
A distributed API for coordinating AbC programs
Coverage-biased random exploration of large models and application to testing
An approach and an Eclipse-based environment for enhancing the navigation structure of Web sites
Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020
Runtime verification: the application perspective
Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard
The PROSPER toolkit
Solving scheduling problems by untimed model checking
Strong Simple Policies for POMDPs
Model-based testing for concurrent systems: unfolding-based test selection
Introduction to the Special Issue devoted to SPIN 2018
Correction to: An integrated specification and verification technique for highly concurrent data structures
Model-based testing of software and systems: recent advances and challenges
Interacting with ETI: A User Session
Testing LTL formula translation into Büchi automata
Mining parametric temporal logic properties in model-based design for cyber-physical systems
Correction to: Correct-by-construction model-based design of reactive streaming software for multi-core embedded systems
Static analysis for discovering IoT vulnerabilities
A taxonomy of risk-based testing
AutoProof: auto-active functional verification of object-oriented programs
Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more
Techniques for modelling and verifying railway interlockings
Modeling task systems using parameterized partial orders
Fully automated runtime enforcement of component-based systems with formal and sound recovery
Efficient monitoring of hyperproperties using prefix trees
Verification and synthesis of co-simulation algorithms subject to algebraic loops and adaptive steps
Functional programming languages for verification tools: a comparison of Standard ML and Haskell
Applying symbolic bounded model checking to the 2012 RERS greybox challenge
Exploring very large state spaces using genetic algorithms
Efficient debugging in a formal verification environment
Formal verification of OIL component specifications using mCRL2
Reducing the size of resolution proofs in linear time
A correct-by-construction model for asynchronously communicating systems
Generating counterexamples of model-based software product lines
Guard-based partial-order reduction
Using an induction prover for verifying arithmetic circuits
High-automation proofs for properties of requirements models
Counting dynamically synchronizing processes
Algorithm selection for SMT
DisCoveR: accurate and efficient discovery of declarative process models
Verification and refutation of C programs based on k-induction and invariant inference
Using static analysis to improve automatic test generation
SMT solvers: new oracles for the HOL theorem prover
Software model checking is a rich research field
Underapproximation of procedure summaries for integer programs
Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY
Dependency graphs with applications to verification
IoT backends in the Asset Administration Shell - four integration approaches
Tools and algorithms for the construction and analysis of systems
A uniform framework for weighted decision diagrams and its implementation
Special section on the 17th International Software Product Line Conference
Symmetry reduction in CSP model checking
Software quality tools and techniques presented in FASE'17
Integrated formal verification of safety-critical software
Policy ignorant caller-side inline reference monitoring
Guest editors' introduction to the special section from the international symposium on web systems evolution
A semantics of communicating reactive objects with timing
A taxonomy for classifying runtime verification tools
Special section on Web Systems Evolution
Constraint-based BMC: a backjumping strategy
An overview of the MOP runtime verification framework
Rigorous engineering of collective adaptive systems: special section
A construction and minimization service for continuous probability distributions
Diagnosing timed automata using timed markings
Algebraically explainable controllers: decision trees and support vector machines join forces
More testable properties
The Clara framework for hybrid typestate analysis
Automatic CoDec generation to reduce test engineering cost
Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (FireWire): An Experiment with E-LOTOS
An ontology for software component matching
Compositional specification of commercial contracts
Program verification and testing technologies
Statistical abstraction and model-checking of large heterogeneous systems
Quantitative modelling and analysis of a Chinese smart grid: a stochastic model checking case study
The common aspect proof environment
Functional synthesis for linear arithmetic and sets
Combining usage-based and model-based testing for service-oriented architectures in the industrial practice
Distributed state space minimization
Some current topics in model checking
Parallel search for LTL violations
Language support for verifying reconfigurable interacting systems
A conformance test suite for TTCN-3 tools - Black-Box functional testing of TTCN-3 syntax and semantics
Leveraging polyhedral reductions for solving Petri net reachability problems
Using simulated execution in verifying distributed algorithms
The role of user requirements in data repository design
Manual and automated performance optimization of model transformation systems
SATMC: a SAT-based model checker for security protocols, business processes, and security APIs
Fast detection of concurrency errors by state space traversal with randomization and early backtracking
Why you should definitely read this special section
Diamont: dynamic monitoring of uncertainty for distributed asynchronous programs
A pilot project for migrating COBOL code to web services
Speeding up static analysis with the split operator
A bit too precise? Verification of quantized digital filters
Preface to the special issue on engineering of computer-based systems
Witnessing the elimination of magic wands
Statistical model checking QoS properties of systems with SBIP
KIV: overview and VerifyThis competition
Variations on parallel explicit emptiness checks for generalized Büchi automata
Assessing the effects of introducing a new software development process: a methodological description
SPIN Model Checking: An Introduction
High-level frameworks for the specification and verification of scheduling problems
First international competition on software testing
SyReNN: A tool for analyzing deep neural networks
Data decision diagrams for Promela systems analysis
Extrapolating (omega-)regular model checking
Automated test generation from timed automata
Compositional verification of real-time systems using Ecdar
PolyGraph: a data flow model with frequency arithmetic
The landing gear system in multi-machine Hybrid Event-B
Expressing checkable properties of dynamic systems: the Bandera Specification Language
Model-driven generation of runtime checks for system properties
Coping with large design spaces: design problem solving in fluidic engineering
Safety first: a two-stage algorithm for the synthesis of reactive systems
Tools for secure systems development with UML
Correct orchestration of federated learning generic algorithms: Python translation to CSP and verification by PAT
A language and framework for dynamic component ensembles in smart systems
Model-checking the preservation of temporal properties upon feature integration
A kinetic approach to investigate the collective dynamics of multi-agent systems
System-on-chip design by proof-based refinement
Issues in Slicing PROMELA and Its Applications to Model Checking, Protocol Understanding, and Simulation
Deductive software verification
Analysing a Mechatronic System with Coloured Petri Nets
Requirements-document-based prototyping of CARA software
Variable order metrics for decision diagrams in system verification
A formal framework for verifying distributed embedded systems based on abstraction methods
Introduction to Selected Papers from SPIN 2017
Program sketching
Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges
Monitoring properties of analog and mixed-signal circuits
Guided search for hybrid systems based on coarse-grained space abstractions
Flexible SAT-based framework for incremental bounded upgrade checking
Probabilistic verification and synthesis of the next generation airborne collision avoidance system
Towards formal methods diversity in railways: an experience report with seven frameworks
Systematic synthesis of delta modeling languages
Modeling and proving functional completeness in formal verification of counting heads
Pragmatics of Model Checking: An STTT Special Section
LTL satisfiability checking
Testing abstract behavioral specifications
Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum
Behavior Analysis for Validating Communication Patterns
Formalization and Validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN
Learning probabilistic models for model checking: an evolutionary approach and an empirical study
Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra
Into the unknown: active monitoring of neural networks (extended version)
MDA-based Automatic OWL Ontology Development
Software engineering practices and Simulink: bridging the gap
Comparison of type-based and alias-based component recognition for embedded systems software
Introductory paper: scalability aspects of validation
Code generation for Event-B
Practical experiences of applying source-level WCET flow analysis to industrial code
Satisfiability checking using Boolean Expression Diagrams
CTL-property Transformations along an Incremental Design Process
An efficient statistical model checker for nondeterminism and rare events
Validation of the Hybrid ERTMS/ETCS Level 3 using Spin
The ABZ-2018 case study with Event-B
(Continuous) Non-malleable Codes for Partial Functions with Manipulation Detection and Light Updates
Probability To Meet in the Middle
Local Randomness in Pseudorandom Sequences
On the Fly Authentication and Signature Schemes Based on Groups of Unknown Order
Analysis and Design of Distributed Key Distribution Centers
Cryptographic Hash Functions from Expander Graphs
General Composition and Universal Composability in Secure Multiparty Computation
Security and Composition of Multiparty Cryptographic Protocols
A Characterization of Chameleon Hash Functions and New, Efficient Designs
Hashing to Elliptic Curves Through Cipolla-Lehmer-Müller's Square Root Algorithm
A New Multivariate Primitive from CCZ Equivalence
The Security of Feistel Ciphers with Six Rounds or Less
A Generalized Correlation Attack on a Class of Stream Ciphers Based on the Levenshtein Distance