Linear Encodings of Bounded LTL Model Checking by Armin Biere, Keijo Heljanko, Tommi Junttila, Timo Latvala, Viktor Schuppan

“…We consider the problem of bounded model checking (BMC) for linear temporal logic (LTL). …”
Get full text

Model Checking Lower Bounds for Simple Graphs by Michael Lampis

“…Second, we show that there is no model-checking algorithm with elementary parameter dependence for MSO logic even restricted to paths (or equivalently to unary strings), unless E=NE. …”
Get full text

Abstracting Strings for Model Checking of C Programs by Henrich Lauko, Martina Olliaro, Agostino Cortesi, Petr Roc̆kai

Subjects: Get full text

Statistical Model Checking for Stochastic Hybrid Systems by Danny Bøgsted Poulsen, Sean Sedwards, Axel Legay, Marius Mikučionis, Kim G. Larsen, Dehui Du, Alexandre David

“…The extensions allow for statistical model checking of stochastic hybrid systems. We show how our race-based stochastic semantics extends to networks of hybrid systems, and indicate the integration technique applied for implementing this semantics in the UPPAAL-SMC simulation engine. …”
Get full text

Intuitionistic implication makes model checking hard by Martin Mundhenk, Felix Weiss

“…We investigate the complexity of the model checking problem for intuitionistic and modal propositional logics over transitive Kripke models. …”
Get full text

Real-Time Model-Checking: Parameters everywhere by Veronique Bruyere, Jean-Francois Raskin

“…In this paper, we study the model-checking and parameter synthesis problems of the logic TCTL over discrete-timed automata where parameters are allowed both in the model (timed automaton) and in the property (temporal formula). …”
Get full text

Using models to model-check recursive schemes by Sylvain Salvati, Igor Walukiewicz

“…We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, lambda-Y-calculus, is equivalent to schemes, we propose the use of a model of lambda-Y-calculus to discriminate the terms that satisfy a given property. …”
Get full text

Faster Existential FO Model Checking on Posets by Jakub Gajarský, Petr Hliněný, Jan Obdržálek, Sebastian Ordyniak

“…We prove that the model checking problem for the existential fragment of first-order (FO) logic on partially ordered sets is fixed-parameter tractable (FPT) with respect to the formula and the width of a poset (the maximum size of an antichain). …”
Get full text

Model Checking Properties on Reduced Trace Systems by Antonella Santone, Gigliola Vaglini

Subjects: Get full text

Declarative symbolic pure-logic model checking by Shlyakhter, Ilya, 1975-

Get full text

Model checking approach to cancer systems biology by Tan, Chun Wei

Get full text

Multi-core model checking algorithm development by Xu, Yi

“…Model checking is an automatic technique for verifying finite state systems. …”
Get full text

Approximate Model Checking of Stochastic Hybrid Systems by Abate, A, Katoen, J, Lygeros, J, Prandini, M

Enhancing Model Checking in Verification by AI Techniques by Buccafurri, F, Eiter, T, Gottlob, G, Leone, N

Assumption-commitment support for CSP model checking by Moffat, N, Goldsmith, M

Watchdog Transformations for Property−Oriented Model−Checking by Goldsmith, M, Moffat, N, Roscoe, B, Whitworth, T, Zakiuddin, I

Computing Over−Approximations with Bounded Model Checking by Kroening, D

Directed Model Checking with Distance−Preserving Abstractions by Dräger, K, Finkbeiner, B, Podelski, A

More effective interpolations in software model checking by Tian, C, Duan, Z, Duan, Z, Ong, C

“…An approach to CEGAR-based model checking which has proved to be successful on large models employs Craig interpolation to efficiently construct parsimonious abstractions. …”

Intersection types and higer-order model checking by Ramsay, S, Steven Ramsay

“…The key is a characterisation of model checking as a problem of intersection type assignment. …”