Hardware verification using software analyzers by Mukherjee, R, Kroening, D, Melham, T

“…We subsequently apply three different software verification techniques -- bounded model checking, path-based symbolic simulation and abstract interpretation -- and compare their performance to conventional methods for property verification of hardware designs at net list and register transfer level. …”

Bisimulations Meet PCTL Equivalences for Probabilistic Automata by Lei Song, Lijun Zhang, Jens Chr. Godskesen, Flemming Nielson

“…Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its extension PCTL^*. …”
Get full text

On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics by Matthias Hoelzel, Richard Wilke

“…We also introduce inclusion-exclusion games that turn out to be precisely the corresponding model-checking games. These games are not only interesting in their own right, but they also are a key factor towards building a bridge between the semantic and syntactic fragments. …”
Get full text

Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence by Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada

“…The work has been motivated by quantitative analysis of the complexity of higher-order model checking.…”
Get full text

A Spatial-Epistemic Logic for Reasoning about Security Protocols by Bernardo Toninho, Luís Caires

“…We also present a model-checking algorithm for our logic, which has been implemented as an extension to the SLMC system.…”
Get full text

Design and Optimisation of the FlyFast Front-end for Attribute-based Coordination by Diego Latella, Mieke Massink

“…The FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individual(s) in the context of very large populations whose global behaviour is approximated using deterministic limit mean-field techniques. …”
Get full text

Verification of Flat FIFO Systems by Alain Finkel, M. Praveen

“…The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. …”
Get full text

Analysis and improvement for authentication protocols of mobile ad hoc network with CSP approach by Li-cai LIU, Li-hua YIN, Yun-chuan GUO, Yan SUN

“…An approach based on the communicating sequential process (CSP) and Model Checking tool FDR was proposed to model and verify a typical authentication protocol of MANET, callced TAM. …”
Get full text

Time-Darts: A Data Structure for Verification of Closed Timed Automata by Jiří Srba, Kim G. Larsen, Kenneth Y. Jørgensen

“…Symbolic data structures for model checking timed systems have been subject to a significant research, with Difference Bound Matrices (DBMs) still being the preferred data structure in several mature verification tools. …”
Get full text

On the Designing of Model Checkers for Real-Time Distributed Systems by D. Yu. Volkanov, V. A. Zakharov, D. A. Zorin, I. V. Konnov, V. V. Podymov

“…To verify real-time properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of real-time systems. One of the most suitable ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. …”
Get full text

Linear-time logics -- a coalgebraic perspective by Corina Cirstea

“…The former semantics is useful for model checking, whereas the latter is the more natural semantics, as it measures the extent with which qualitative properties hold along computation paths from a given state. …”
Get full text

Representing Strategies by Hein Duijf, Jan Broersen

“…Leaving differences between strategy types implicit in the semantics is a sensible idea if the goal is to use the strategic formalism for model checking. But, for traditional knowledge representation in terms of object language level formulas, we need to extent the language. …”
Get full text

Reasoning about Strategies: on the Satisfiability Problem by Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi

“…Unfortunately, due to its high expressiveness, SL has a non-elementarily decidable model-checking problem and the satisfiability question is undecidable, specifically Sigma_1^1. …”
Get full text

Diagnostics for stochastic genome-scale modeling via model slicing and debugging. by Kevin J Tsai, Chuan-Hsiung Chang

“…We then compared the advantages of our methodology over other modeling techniques such as model checking and model reduction. A software application that implements the methodology is available at http://gel.ym.edu.tw/gcs/.…”
Get full text

Verifying Real-Time Systems using Explicit-time Description Methods by Hao Wang, Wendy MacCaull

“…Timed model checking has been extensively researched in recent years. …”
Get full text

Goodness-of-fit tests for weibull populations on the basis of records by Mahdi Doostparast

“…Consequently, formal hypothesis tests are an important part of model checking (Lawless, 2003). In this paper, Kolmogorov-Smirnov and Cramer-von Mises type goodness of fit tests for record data are pro- posed. …”
Get full text

A Case Study on Formal Verification of Self-Adaptive Behaviors in a Decentralized System by M. Usman Iftikhar, Danny Weyns

“…In this paper, we present a case study in which we use model checking to verify behavioral properties of a decentralized self-adaptive system. …”
Get full text

On the Expressiveness and Complexity of ATL by Francois Laroussinie, Nicolas Markey, Ghassan Oreiby

“…In this paper, we first precisely characterize the complexity of ATL model-checking over Alternating Transition Systems and Concurrent Game Structures when the number of agents is not fixed. …”
Get full text

Verification of railway interlocking systems by Simon Busard, Quentin Cappart, Christophe Limbrée, Charles Pecheur, Pierre Schaus

“…Finally we show how we could verify a realistic set of safety properties on a real-size station model by customizing the existing model-checking algorithm with PyNuSMV a Python library based on NuSMV.…”
Get full text

Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report by Étienne André, Mohamed Mahdi Benmoussa, Christine Choppy

“…However its semantics is described informally, thus preventing the application of model checking techniques that could guarantee the system safety. …”
Get full text