Search
Search Results
-
A general model-checking procedure for semiparametric accelerated failure time models
We propose a set of goodness-of-fit tests for the semiparametric accelerated failure time (AFT) model, including an omnibus test, a link function...
-
Symbolic Model Checking for TLA+ Made Faster
The need to provide formal guarantees about the behaviour of the algorithms underpinning modern distributed systems became evident in recent years....
-
Model Checking Software 27th International Symposium, SPIN 2021, Virtual Event, July 12, 2021, Proceedings
This book constitutes the refereed proceedings of the 27th International Symposium on Model Checking Software, SPIN 2021, held virtually in July 2021.
-
Base-Based Model Checking for Multi-agent only Believing
We present a novel semantics for the language of multi-agent only believing exploiting belief bases, and show how to use it for automatically...
-
Multi-agent Verification and Control with Probabilistic Model Checking
Probabilistic model checking is a technique for formal automated reasoning about software or hardware systems that operate in the context of...
-
Accelerated Bounded Model Checking Using Interpolation Based Summaries
We propose a novel lazy bounded model checking (BMC) algorithm, Trace Inlining, that identifies relevant behaviors of the program to compute partial...
-
Model Checking Reversible Systems: Forwardly
Reversibility is nowadays playing a major role when dealing with systems, allowing to revert to safe states of systems evolutions. For instance...
-
PYGC: A PinYin Language Model Guided Correction Model for Chinese Spell Checking
Chinese Spell Checking (CSC) is an NLP task that detects and corrects erroneous characters in Chinese texts. Since people often use pinyin...
-
Optimal Stateless Model Checking for Causal Consistency
We present a framework for efficient stateless model checking (SMC) of concurrent programs under three prominent models of causal consistency,...
-
A JPSL Based Model Checking Approach for Java Programs
In order to verify the correctness of Java programs, a model checking approach that accurately verifies the properties of Java is advocated. To this...
-
Fast Verified SCCs for Probabilistic Model Checking
High-performance probabilistic model checkers like the Modest Toolset’s mcsta follow the topological ordering of an MDP’s strongly connected...
-
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about...
-
Searching for i-Good Lemmas to Accelerate Safety Model Checking
IC3/PDR and its variants have been the prominent approaches to safety model checking in recent years. Compared to the previous model-checking...
-
Petrification: Software Model Checking for Programs with Dynamic Thread Management
We address the verification problem for concurrent program that dynamically create (fork) new threads or destroy (join) existing threads. We present...
-
Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
Automated driving functions are among the most critical software components to develop. Before deployment in series vehicles, it has to be shown that...
-
Compositional Probabilistic Model Checking with String Diagrams of MDPs
We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language...
-
On the Model Checking Problem for Some Extension of CTL*
AbstractSequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output...
-
Model Checking for Entanglement Swap**
Entanglement swap** is a basic primitive in long distance quantum communications. The stochastic nature of various operations like entanglement...
-
Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking
Parametric verification of linear temporal properties for stochastic models requires to compute the satisfaction probability of a certain property as...
-
FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format
We present FuzzBtor2, a fuzzer to generate random word-level model checking problems in Btor2 format. Btor2 is one of the mainstream input formats...