Faster FDR Counterexample Generation Using SAT−Solving

Faster FDR Counterexample Generation Using SAT−Solving

With the flourishing development of efficient SAT-solvers, bounded model checking (BMC) has proven to be an extremely powerful symbolic model checking technique. In this paper, we address the problem of applying BMC to concurrent systems involving the interaction of multiple processes running in par...

Полное описание

Библиографические подробности
Главные авторы:	Palikareva, H, Ouaknine, J, Roscoe, A
Другие авторы:	Roggenbach, M
Формат:	Journal article
Опубликовано:	2009

Схожие документы

SAT solving in CSP trace refinement
по: Palikareva, H, и др.
Опубликовано: (2012)

SAT−solving in CSP trace refinement
по: Palikareva, H, и др.
Опубликовано: (2011)

SAT−Solving in CSP Trace Refinement
по: Palikareva, H, и др.
Опубликовано: (2012)

SAT-solving in CSP trace refinement
по: Palikareva, H, и др.
Опубликовано: (2012)

Recent developments in FDR
по: Armstrong, P, и др.
Опубликовано: (2012)

Recent developments in FDR
по: Armstrong, P, и др.
Опубликовано: (2012)

Recent developments in FDR
по: Armstrong, P, и др.
Опубликовано: (2012)

Recent Developments in FDR
по: Armstrong, P, и др.
Опубликовано: (2012)

FDR into The Cloud
по: Gibson−Robinson, T, и др.
Опубликовано: (2014)

Verifying Statemate Statecharts Using CSP and FDR
по: Roscoe, A, и др.
Опубликовано: (2006)

Modelling and verifying key−exchange protocols using CSP and FDR
по: Roscoe, A
Опубликовано: (1995)

Compiling Statemate Statecharts into CSP and verifying them using FDR
по: Roscoe, A
Опубликовано: (2003)

FDR2 user manual
по: Gardiner, P, и др.
Опубликовано: (2000)

Verifying an infinite family of inductions simultaneously using data independence and FDR
по: Roscoe, A, и др.
Опубликовано: (1999)

Parallelization of FDR
по: Goldsmith, M, и др.
Опубликовано: (2002)

Web Services Security: a preliminary study using Casper and FDR
по: Roscoe, A, и др.
Опубликовано: (2004)

FDR3 — A Modern Refinement Checker for CSP
по: Gibson−Robinson, T, и др.
Опубликовано: (2014)

Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving
по: Antonino, P, и др.
Опубликовано: (2019)

Counterexample guided program repair using zero-shot learning and MaxSAT-based fault localization
по: Orvalho, P, и др.
Опубликовано: (2025)

Efficient verification of comcurrent systems using local analysis based approximations and SAT solving
по: Antonino, P, и др.
Опубликовано: (2019)

Counter abstraction in the CSP/FDR setting
по: Mazur, T, и др.
Опубликовано: (2009)

Counter Abstraction in the CSP/FDR setting
по: Mazur, T, и др.
Опубликовано: (2007)

Inside FDR (abstract of invited talk)
по: Goldsmith, M
Опубликовано: (2012)

Understanding Counterexamples with explain
по: Groce, A, и др.
Опубликовано: (2004)

On counterexamples to the Hughes conjecture
по: Havas, G, и др.
Опубликовано: (2009)

Solving reaction-diffusion equations 10 times faster
по: Kassam, A
Опубликовано: (2003)

Static Livelock Analysis in CSP
по: Ouaknine, J, и др.
Опубликовано: (2011)

Static livelock analysis in CSP
по: Ouaknine, J, и др.
Опубликовано: (2011)

A Static Analysis Framework for Livelock Freedom in CSP
по: Ouaknine, J, и др.
Опубликовано: (2013)

A Static Analysis Framework for Livelock Freedom in CSP
по: Ouaknine, J, и др.
Опубликовано: (2013)

A Static Analysis Framework for Livelock Freedom in CSP
по: Ouaknine, J, и др.
Опубликовано: (2012)

Static Livelock Analysis in CSP
по: Ouaknine, J, и др.
Опубликовано: (2011)

Critical systems validation and verification with CSP and FDR
по: Goldsmith, M, и др.
Опубликовано: (1999)

Logic for fun : solving puzzles with SAT solvers
по: Foo, Zhong Xian
Опубликовано: (2016)

Analyzing a Library of Security Protocols using Casper and FDR
по: Donovan, B, и др.
Опубликовано: (1999)

Making the most of BMC counterexamples
по: Groce, A, и др.
Опубликовано: (2005)

Making the Most of BMC Counterexamples
по: Groce, A, и др.
Опубликовано: (2005)

Empirical analysis and optimization of an NP−hard problem using CSP and FDR
по: Creager, D, и др.
Опубликовано: (2007)

A counterexample to metric differentiability
по: Kirchheim, B, и др.
Опубликовано: (2003)

Counterexample−guided Precondition Inference
по: Seghir, M, и др.
Опубликовано: (2013)