
WebTLR
 Referenced in 8 articles
[sw09905]
 software tool designed for modelchecking Web applications which is based on rewriting logic...

Alloy
 Referenced in 29 articles
[sw01247]
 Alloy is a lightweight language for software modelling. It’s designed to be flexible ... amenable to fully automatic simulation and checking. At its core, Alloy is a simple first...

AGG
 Referenced in 49 articles
[sw04449]
 validations which comprise graph parsing, consistency checking of graphs and conﬂict detection in concurrent transformations ... include graph and rulebased modeling of software, validation of system properties by assigning...

EUREKA
 Referenced in 3 articles
[sw20979]
 Eureka Tool for Software Model Checking. We describe EUREKA, a symbolic model checker for Linear...

jMocha
 Referenced in 3 articles
[sw24777]
 automated debugging of embedded software. In model checking, a highlevel description of a system ... model checker jMocha (Java MOdelCHecking Algorithm) is based on this theme. Instead of manipulating ... hierarchical modeling framework of reactive modules. jMocha is a growing interactive software environment for specification ... verification both by symbolic and enumerative model checking; (4) implementation verification by checking trace containment...

ESBMC
 Referenced in 7 articles
[sw09946]
 contextbounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver ... verify single and multithreaded software (with shared variables and locks); (ii) to reason about ... properties using assertstatements, that are then checked as well. It also provides three approaches ... underapproximation and widening) to model check multithreaded software. ESBMC can be invoked through...

Wolf
 Referenced in 2 articles
[sw01299]
 methods complement explicit exploration methods of software model checking...

SIMP
 Referenced in 2 articles
[sw09936]
 Specialization with constrained generalization for software model checking. We present a method for verifying properties ... operator and we address the problem of checking whether or not a safety property ... deriving, if possible, a program whose least model is a finite set of constrained facts ... with respect to stateoftheart software model checkers...

SymmPa
 Referenced in 3 articles
[sw08414]
 CEGAR) have enabled finitestate model checking of software written in mainstream programming languages. This ... applications of CEGAR to sharedvariable concurrent software. We attribute this gap to the lack ... original concurrent program. State explosion during model checking parallel instantiations of this template...

UCLID
 Referenced in 25 articles
[sw04657]
 hardware and software systems. UCLID can be used to model and verify infinitestate systems ... verifier, for termlevel bounded model checking, correspondence checking, deductive verification, and predicate abstractionbased ... date include microprocessor design verification, analyzing software for security exploits, and verifying distributed algorithms...

Gauss
 Referenced in 2 articles
[sw08835]
 avenues for problem driven advances in software modelchecking applied to scientific computing software development...

TravMC
 Referenced in 1 article
[sw09396]
 serve as a basis for software model checking for functional languages such...

EUFORIA
 Referenced in 1 article
[sw31587]
 EUFORIA: complete software model checking with uninterpreted functions. We introduce and evaluate an algorithm ... style software model checker that operates entirely at the level of equality with uninterpreted functions...

DC2
 Referenced in 1 article
[sw15730]
 scalable, scopebounded software verification. Software model checking and static analysis have matured over ... last decade, enabling their use in automated software verification. However, lack of scalability makes these ... hard to apply. Furthermore, approximations in the models of program and environment lead...

JayHorn
 Referenced in 1 article
[sw25903]
 JayHorn is a software model checking tool for Java. JayHorn tries to find a proof...

ObjectCheck
 Referenced in 2 articles
[sw00645]
 Specifying software system designs with executable objectoriented modeling languages such as XUML, an executable ... verifying these system designs by model checking. However, stateoftheart model checkers ... software system designs due to the semantic and syntactic gaps between executable objectoriented modeling ... supports an approach to model checking executable objectoriented software system designs modeled in xUML...

DeltaCCS
 Referenced in 4 articles
[sw14476]
 Incremental model checking of deltaoriented software product lines. We propose DeltaCCS, a deltaoriented ... calculus CCS to formalize behavioral variability in software product line specifications in a modular ... propose a novel approach for incremental model checking of product lines. Therefore, variabilityaware congruence...

SMART_
 Referenced in 33 articles
[sw04097]
 describe the main features of Smart, a software package providing a seamless environment ... combine different formalisms in the same modeling study. For the analysis of logical behavior, both ... techniques, as well as symbolic CTL modelchecking algorithms, are available. For the study...

MoCHi
 Referenced in 9 articles
[sw21478]
 software model checker for a subset of OCaml. MoCHi is based on higherorder model ... checking, predicate abstraction, and CEGAR (see this paper for details...

Vensim
 Referenced in 14 articles
[sw12336]
 Vensim is simulation software for improving the performance of real systems. Vensim is used ... dynamic feedback models. We emphasize: High quality, with dimensional consistency and Reality Checks™. Connections...