Stem checker$ (all stems)

175 papers:

TACAS-2015-CimattiGMT #hybrid #model checking #named #smt

HyComp: An SMT-Based Model Checker for Hybrid Systems (AC, AG, SM, ST), pp. 52–67.

FM-2015-FengHTZ #model checking #named #protocol #quantum #source code

QPMC: A Model Checker for Quantum Programs and Protocols (YF, EMH, AT, LZ), pp. 265–272.

Onward-2015-GreweEWM #performance #proving #type system

Type systems for the masses: deriving soundness proofs and efficient checkers (SG, SE, PW, MM), pp. 137–150.

SPLC-2015-DimovskiABW #model checking #off the shelf #using

Family-based model checking using off-the-shelf model checkers: extended abstract (ASD, ASAS, CB, AW), p. 397.

CAV-2015-MajumdarW #bound #model checking #named #source code

Bbs: A Phase-Bounded Model Checker for Asynchronous Programs (RM, ZW), pp. 496–503.

ICST-2015-ZhangAC #exclamation #model checking #verification

Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications (HZ, TA, YC), pp. 1–10.

TACAS-2014-ArmandoCC #model checking #named #satisfiability

SATMC: A SAT-Based Model Checker for Security-Critical Systems (AA, RC, LC), pp. 31–45.

TACAS-2014-Gibson-RobinsonABR #csp #named #refinement

FDR3 — A Modern Refinement Checker for CSP (TGR, PJA, AB, AWR), pp. 187–201.

TACAS-2014-KroeningT #bound #c #contest #model checking #named

CBMC — C Bounded Model Checker — (Competition Contribution) (DK, MT), pp. 389–391.

TACAS-2014-MullerV #contest #named

CPAlien: Shape Analyzer for CPAChecker — (Competition Contribution) (PM, TV), pp. 395–397.

MSR-2014-TulsianKKLN #algorithm #model checking #named

MUX: algorithm selection for software model checkers (VT, AK, RK, AL, AVN), pp. 132–141.

PLDI-2014-BiswasHSB #named #performance #precise

DoubleChecker: efficient sound and precise atomicity checking (SB, JH, AS, MDB), p. 6.

FM-2014-HahnLSTZ #model checking #named #probability

iscasMc: A Web-Based Probabilistic Model Checker (EMH, YL, SS, AT, LZ), pp. 312–317.

SEFM-2014-DobrikovL #model checking #optimisation #partial order #reduction #using

Optimising the ProB Model Checker for B Using Partial Order Reduction (ID, ML), pp. 220–234.

SEFM-2014-MotaFDW #agile #model checking #prototype #semantics

Rapid Prototyping of a Semantically Well Founded Circus Model Checker (AM, AF, AD, JW), pp. 235–249.

SEKE-2014-OrtinPQG #framework #implementation #named #object-oriented

TyS — A Framework to Facilitate the Implementation of Object-Oriented Type Checkers (FO, DZP, JQ, MG), pp. 150–155.

FSE-2014-LiYP0H #finite #infinity #ltl #named #satisfiability

Aalta: an LTL satisfiability checker over Infinite/Finite traces (JL, YY, GP, LZ, JH), pp. 731–734.

CGO-2014-YanXYR #detection #memory management #named

LeakChecker: Practical Static Memory Leak Detection for Managed Languages (DY, G(X, SY, AR), p. 87.

CAV-2014-CavadaCDGMMMRT #model checking

The nuXmv Symbolic Model Checker (RC, AC, MD, AG, AM, AM, SM, MR, ST), pp. 334–342.

CAV-2014-CermakLMM #logic #model checking #named #specification #verification

MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PC, AL, FM, AM), pp. 525–532.

ISSTA-2014-WeitzSKE #java #string

A format string checker for Java (KW, SS, GK, MDE), pp. 441–444.

ECSA-2013-SilvaB #architecture #automation #consistency #named

PANDArch: A Pluggable Automated Non-intrusive Dynamic Architecture Conformance Checker (LdS, DB), pp. 240–248.

ASE-2013-FalkeMS #bound #model checking

The bounded model checker LLBMC (SF, FM, CS), pp. 706–709.

DAC-2013-WangK #control flow #detection #hardware #kernel #named #performance #using

NumChecker: detecting kernel control-flow modifying rootkits by using hardware performance counters (XW, RK), p. 7.

TACAS-2013-ChenFKPS #game studies #model checking #multi #named #probability

PRISM-games: A Model Checker for Stochastic Multi-Player Games (TC, VF, MZK, DP, AS), pp. 185–191.

TACAS-2013-FedyukovichSS #c #incremental #named

eVolCheck: Incremental Upgrade Checker for C (GF, OS, NS), pp. 292–307.

PEPM-2013-SatoUK #higher-order #model checking #scalability #source code #towards

Towards a scalable software model checker for higher-order programs (RS, HU, NK), pp. 53–62.

IFL-2013-Protzenko #implementation

The implementation of the Mezzo type-checker (JP), p. 129.

SAC-2013-RenTSF #ruby

The ruby type checker (BMR, JT, TSS, JSF), pp. 1565–1572.

ESEC-FSE-2013-LiuL0ZWD #model checking #named #self #state machine #uml

USMMC: a self-contained model checker for UML state machines (SL, YL, JS, MZ, BW, JSD), pp. 623–626.

ICSE-2013-DongSL #model checking

Build your own model checker in one month (JSD, JS, YL), pp. 1481–1483.

CAV-2013-BarnatBHHKLRSW #c #c++ #model checking #parallel #source code #thread

DiVinE 3.0 — An Explicit-State Model Checker for Multithreaded C & C++ Programs (JB, LB, VH, JH, JK, ML, PR, VS, JW), pp. 863–868.

CAV-2013-ChengRS #constraints #named #polynomial

JBernstein: A Validity Checker for Generalized Polynomial Constraints (CHC, HR, NS), pp. 656–661.

CAV-2013-EsparzaLNNSS #execution #ltl #model checking

A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.

ICST-2013-Torsel #domain-specific language #model checking #modelling #testing #using #web

A Testing Tool for Web Applications Using a Domain-Specific Modelling Language and the NuSMV Model Checker (AMT), pp. 383–390.

ASE-2012-SongT #model checking #named #source code

PuMoC: a CTL model-checker for sequential programs (FS, TT), pp. 346–349.

DATE-2012-MammoCPNZMB #approximate #simulation

Approximating checkers for simulation acceleration (BM, DC, DP, AN, AZ, RM, VB), pp. 153–158.

TACAS-2012-SinzMF #bound #contest #model checking #named #representation

LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation — (Competition Contribution) (CS, FM, SF), pp. 542–544.

SAC-2012-PerroneDH #graph #model checking

A model checker for Bigraphs (GP, SD, TTH), pp. 1320–1325.

CAV-2012-ConchonGKMZ #model checking #named #parallel #smt

Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems — Tool Paper (SC, AG, SK, AM, FZ), pp. 718–724.

CAV-2012-HopkinsMO #equivalence #higher-order #ml #named

Hector: An Equivalence Checker for a Higher-Order Fragment of ML (DH, ASM, CHLO), pp. 774–780.

CAV-2012-SongSLD #model checking #probability #realtime

A Model Checker for Hierarchical Probabilistic Real-Time Systems (SS, JS, YL, JSD), pp. 705–711.

ICST-2012-GligoricMM #model checking #named #programming language

X10X: Model Checking a New Programming Language with an “Old” Model Checker (MG, PCM, DM), pp. 11–20.

ICALP-v2-2011-ZhangB #model checking #probability

A Progress Measure for Explicit-State Probabilistic Model-Checkers (XZ, FvB), pp. 283–294.

ICSE-2011-DietlDEMS #using

Building and using pluggable type-checkers (WD, SD, MDE, KM, TWS), pp. 681–690.

CAV-2011-CimattiGMNR #model checking #named

Kratos — A Software Model Checker for SystemC (AC, AG, AM, IN, MR), pp. 310–316.

ICST-2011-SaifanDBP #consistency #implementation #mobile #runtime

Implementing and Evaluating a Runtime Conformance Checker for Mobile Agent Systems (AAS, JD, JSB, EP), pp. 269–278.

DATE-2010-BuLWCL #bound #composition #hybrid #linear #reachability

BACH 2 : Bounded reachability checker for compositional linear hybrid systems (LB, YL, LW, XC, XL), pp. 1512–1517.

DATE-2010-GuglielmoFP #analysis

Vacuity analysis for property qualification by mutation of checkers (LDG, FF, GP), pp. 478–483.

TACAS-2010-DragerKFW #concurrent #infinity #model checking #named

SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems (KD, AK, BF, HW), pp. 271–274.

WRLA-2010-BaeM #linear #logic #maude #model checking

The Linear Temporal Logic of Rewriting Maude Model Checker (KB, JM), pp. 208–225.

WRLA-2010-DuranM #equation #maude #order #specification

A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications (FD, JM), pp. 69–85.

WRLA-2010-DuranM10a #maude #order

A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories (FD, JM), pp. 86–103.

PLDI-2010-BurckhardtDMT #automation #named

Line-up: a complete and automatic linearizability checker (SB, CD, MM, RT), pp. 330–340.

SEFM-2010-HussainL #ml #named #runtime #specification

temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties (FH, GTL), pp. 63–72.

LDTA-2010-BrandMSH #case study #domain-specific language #experience

Formally specified type checkers for domain specific languages: experience report (MvdB, APvdM, AS, ATH), p. 12.

CAV-2010-BozzanoCKNNRW #model checking

A Model Checker for AADL (MB, AC, JPK, VYN, TN, MR, RW), pp. 562–565.

CAV-2010-Caniart #model checking #named

Merit: An Interpolating Model-Checker (NC), pp. 162–166.

CAV-2010-HahnHWZ #markov #model checking #modelling #named #parametricity

PARAM: A Model Checker for Parametric Markov Models (EMH, HH, BW, LZ), pp. 660–664.

IJCAR-2010-GhilardiR #model checking #modulo theories #named

MCMT: A Model Checker Modulo Theories (SG, SR), pp. 22–29.

ESOP-2009-SadowskiFF #named #parallel #source code #thread

SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs (CS, SNF, CF), pp. 394–409.

TACAS-2009-LimeRST #model checking #named #parametricity #petri net

Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches (DL, OHR, CS, LMT), pp. 54–57.

CAV-2009-HahnHWZ #infinity #markov #model checking #named

INFAMY: An Infinite-State Markov Model Checker (EMH, HH, BW, LZ), pp. 641–647.

CAV-2009-HopkinsO #equivalence #higher-order #model checking #named

Homer: A Higher-Order Observational Equivalence Model checkER (DH, CHLO), pp. 654–660.

CAV-2009-LomuscioQR #model checking #multi #named #verification

MCMAS: A Model Checker for the Verification of Multi-Agent Systems (AL, HQ, FR), pp. 682–688.

ICST-2009-FraserG #evaluation #generative #model checking #specification #testing

An Evaluation of Model Checkers for Specification Based Test Case Generation (GF, AG), pp. 41–50.

QoSA-2008-PlsekA #component #model checking #named

Carmen: Software Component Model Checker (AP, JA), pp. 71–85.

ASE-2008-KimKK #memory management #model checking #satisfiability #testing

Unit Testing of Flash Memory Device Driver through a SAT-Based Model Checker (MK, YK, HK), pp. 198–207.

CSEET-2008-SalamahG #education #model checking #specification #using

A Technique for Using Model Checkers to Teach Formal Specifications (SS, AQG), pp. 181–188.

SCAM-2008-Cifuentes #c #debugging #named #scalability

Parfait — A Scalable Bug Checker for C Code (CC), pp. 263–264.

PLDI-2008-FlanaganFY #named #parallel #source code #thread

Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs (CF, SNF, JY), pp. 293–303.

ICSE-2008-LongDG #experience #industrial #model checking

Experience applying the SPIN model checker to an industrial telecommunications system (BL, JD, TCNG), pp. 693–702.

OSDI-2008-GunawiRAA #declarative #file system #named

SQCK: A Declarative File System Checker (HSG, AR, ACAD, RHAD), pp. 131–146.

CAV-2008-GayNP #model checking #named #quantum

QMC: A Model Checker for Quantum Systems (SJG, RN, NP), pp. 543–547.

IJCAR-2008-BoyerGJ #automaton

Certifying a Tree Automata Completion Checker (BB, TG, TPJ), pp. 523–538.

ASE-2007-KuHCL #benchmark #metric #model checking

A buffer overflow benchmark for software model checkers (KK, TEH, MC, DL), pp. 389–392.

ITiCSE-2007-StallmannBRBGH #automaton #correctness #named #proving

ProofChecker: an accessible environment for automata theory correctness proofs (MFS, SB, RDR, SB, MCG, SDH), pp. 48–52.

FASE-2007-BachFS #eclipse #plugin #programming

Declared Type Generalization Checker: An Eclipse Plug-In for Systematic Programming with More General Types (MB, FF, FS), pp. 117–120.

SAS-2007-ChangRN #analysis #invariant

Shape Analysis with Structural Invariant Checkers (BYEC, XR, GCN), pp. 384–401.

IFM-2007-PlaggeL #model checking #specification #using #validation

Validating Z Specifications Using the ProBAnimator and Model Checker (DP, ML), pp. 480–500.

ICFP-2007-FredlundS #distributed #functional #model checking #named #programming language

McErlang: a model checker for a distributed functional programming language (LÅF, HS), pp. 125–136.

AMOST-2007-FraserW #generative #ltl #model checking #performance #testing #using

Using LTL rewriting to improve the performance of model-checker based test-case generation (GF, FW), pp. 64–74.

MBT-2007-BorodayPG #model checking #nondeterminism #question #testing

Can a Model Checker Generate Tests for Non-Deterministic Systems? (SB, AP, RG), pp. 3–19.

MBT-2007-FraserAW #model checking #testing

Handling Model Changes: Regression Testing and Test-Suite Update with Model-Checkers (GF, BKA, FW), pp. 33–46.

MBT-2007-RaimondiPB #model checking #testing

Testing Planning Domains (without Model Checkers) (FR, CP, GB), pp. 113–125.

SAT-2007-JussilaBSKW #proving #towards

A First Step Towards a Unified Proof Checker for QBF (TJ, AB, CS, DK, CMW), pp. 201–214.

ASE-2006-LiuYR #library #model checking #using

Software Library Usage Pattern Extraction Using a Software Model Checker (CL, EY, DJR), pp. 301–304.

DATE-2006-SrinivasanTC #automation #low cost #multi #online

Online RF checkers for diagnosing multi-gigahertz automatic test boards on low cost ATE platforms (GS, FT, AC), pp. 658–663.

TACAS-2006-LomuscioR #model checking #multi #named

MCMAS: A Model Checker for Multi-agent Systems (AL, FR), pp. 450–454.

FM-2006-HuynhR #c# #memory management

A Memory Model Sensitive Checker for C# (TQH, AR), pp. 476–491.

QAPL-2005-KwiatkowskaNP06 #analysis #model checking #probability

Quantitative Analysis With the Probabilistic Model Checker PRISM (MZK, GN, DP), pp. 5–31.

PADL-2006-Wang #automation #model checking #verification

Automatic Verification of a Model Checker by Reflection (BYW), pp. 45–59.

AMOST-J-2005-Robinson-MallettLMG06 #identification #model checking #using #verification

Extended state identification and verification using a model checker (CRM, PL, TM, UG), pp. 981–992.

CAV-2006-GurfinkelWC #model checking #named #verification

Yasm: A Software Model-Checker for Verification and Refutation (AG, OW, MC), pp. 170–174.

CAV-2006-SethiB #c #deduction #named

cascade: C Assertion Checker and Deductive Engine (NS, CB), pp. 166–169.

IJCAR-2006-HendrixMO #axiom #linear #order #specification

A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms (JH, JM, HO), pp. 151–155.

RTA-2006-WehrmanSW #named #termination

Slothrop: Knuth-Bendix Completion with a Modern Termination Checker (IW, AS, EMW), pp. 287–296.

WRLA-2004-PalominoP05 #maude #model checking #proving

Proving VLRL Action Properties with the Maude Model Checker (MP, IP), pp. 113–133.

ESOP-2005-NaikP #model checking #type system

A Type System Equivalent to a Model Checker (MN, JP), pp. 374–388.

TACAS-2005-SuwimonteerabuthSE #bytecode #java #named

jMoped: A Java Bytecode Checker Based on Moped (DS, SS, JE), pp. 541–545.

SEFM-2005-NivelleP #verification

Verification of an Off-Line Checker for Priority Queues (HdN, RP), pp. 210–219.

SEKE-2005-Wang #infinity #logic #model checking #specification

Specification of an Infinite-State Local Model Checker in Rewriting Logic (BYW), pp. 442–447.

SAC-2005-BalsaraR #model checking #predict #search-based #using

Prediction of inherited and genetic mutations using the software model checker SPIN (ZB, SR), pp. 208–209.

AMOST-2005-Robinson-MallettLMG #generative #model checking #sequence

Generating optimal distinguishing sequences with a model checker (CRM, PL, TM, UG).

CAV-2005-DwyerHHR #framework #model checking #using

Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework (MBD, JH, MH, R), pp. 148–152.

CAV-2005-Younes05a #model checking #named #statistics

Ymer: A Statistical Model Checker (HLSY), pp. 429–433.

TACAS-2004-PiazzaPR #named #persistent #security

CoPS — Checker of Persistent Security (CP, EP, SR), pp. 144–152.

SEFM-2004-HamonMR #generative #model checking #performance #testing

Generating Efficient Test Sets with a Model Checker (GH, LMdM, JMR), pp. 261–270.

POPL-2004-FlanaganF #named #parallel #source code #thread

Atomizer: a dynamic atomicity checker for multithreaded programs (CF, SNF), pp. 256–267.

ICSE-2004-GouldSD04a #sql #static analysis

JDBC Checker: A Static Analysis Tool for SQL/JDBC Applications (CG, ZS, PTD), pp. 697–698.

CAV-2004-AndrewsQRRX #concurrent #model checking #named

Zing: A Model Checker for Concurrent Software (TA, SQ, SKR, JR, YX), pp. 484–487.

CAV-2004-BarrettB #implementation

CVC Lite: A New Implementation of the Cooperating Validity Checker Category B (CWB, SB), pp. 515–518.

CAV-2004-GriffaultV #model checking

The Mec 5 Model-Checker (AG, AV), pp. 488–491.

DAC-2003-TasiranYB #model checking #monitoring #simulation #specification #using

Using a formal specification and a model checker to monitor and direct simulation (ST, YY, BB), pp. 356–361.

DATE-2003-OmanaRM #parallel

High Speed and Highly Testable Parallel Two-Rail Code Checker (MO, DR, CM), pp. 10608–10615.

DATE-2003-Tarnick #embedded #self

Self-Testing Embedded Checkers for Bose-Lin, Bose, and a Class of Borden Codes (ST), pp. 11162–11163.

DATE-2003-ZhangM #implementation #independence #satisfiability #using #validation

Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications (LZ, SM), pp. 10880–10885.

FME-2003-LeuschelB #model checking #named

ProB: A Model Checker for B (ML, MJB), pp. 855–874.

PPDP-2003-WuAS #proving

Foundational proof checkers with small witnesses (DW, AWA, AS), pp. 264–274.

ICSE-2003-EasterbrookCDGLPTT #model checking #multi #named #reasoning

χChek: A Model Checker for Multi-Valued Reasoning (SME, MC, BD, AG, AYCL, VP, AT, CDTW), pp. 804–805.

CAV-2003-ChechikG #logic #named #query

TLQSolver: A Temporal Logic Query Checker (MC, AG), pp. 210–214.

FATES-2003-HeimdahlRVDG #case study #model checking #sequence #testing #using

Auto-generating Test Sequences Using Model Checkers: A Case Study (MPEH, SR, WV, GD, JG), pp. 42–59.

VMCAI-2003-CatanoH #ml #named #static analysis

CHASE: A Static Checker for JML’s Assignable Clause (NC, MH), pp. 26–40.

CBSE-2003-Heineman #component #interface #modelling

Integrating Interface Assertion Checkers into Component Models (GTH), p. 9.

WRLA-2002-EkerMS #ltl #maude #model checking

The Maude LTL Model Checker (SE, JM, AS), pp. 162–187.

PASTE-2002-ChelfEH #how #static analysis

How to write system-specific, static checkers in metal (BC, DRE, SH), pp. 51–60.

FME-2002-HuberK #model checking #towards

Towards an Integrated Model Checker for Railway Signalling Data (MH, SK), pp. 204–223.

ICSE-2002-SchapachnikBO #approach #architecture #automaton #development #distributed #model checking

An architecture-centric approach to the development of a distributed model-checker for timed automata (FS, VAB, AO), p. 710.

CAV-2002-ChechikGD #model checking #multi #named

chi-Chek: A Multi-valued Model-Checker (MC, AG, BD), pp. 505–509.

CAV-2002-FlanaganQS #composition #parallel #source code #thread

A Modular Checker for Multithreaded Programs (CF, SQ, SAS), pp. 180–194.

CAV-2002-GrocePY #adaptation #model checking #named

AMC: An Adaptive Model Checker (AG, DP, MY), pp. 521–525.

CAV-2002-StumpBD #named

CVC: A Cooperating Validity Checker (AS, CWB, DLD), pp. 500–504.

SAT-2002-MalerMNA #difference #logic #satisfiability

A satisfiability checker for difference logic (OM, MM, PN, EA), p. 27.

TACAS-2001-ChechikDE #implementation #model checking #multi

Implementing a Multi-valued Symbolic Model Checker (MC, BD, SME), pp. 404–419.

PADL-2001-Kaser #generative #model checking

State Generation in the PARMC Model Checker (OK), pp. 337–352.

PADL-2001-Ramakrishnan #calculus #logic programming #model checking #using #μ-calculus

A Model Checker for Value-Passing μ-Calculus Using Logic Programming (CRR), pp. 1–13.

CC-2001-MartenaP #alias #analysis #model checking

Alias Analysis by Means of a Model Checker (VM, PSP), pp. 3–19.

CAV-2001-EsparzaS #model checking #recursion #source code

A BDD-Based Model Checker for Recursive Programs (JE, SS), pp. 324–336.

CAV-2001-Namjoshi #model checking

Certifying Model Checkers (KSN), pp. 2–13.

CAV-2001-VelevB #logic #named #similarity

EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations (MNV, REB), pp. 235–240.

DATE-2000-VardanianM #concurrent #detection #fault

Improving the Error Detection Ability of Concurrent Checkers by Observation Point Insertion in the Circuit Under Check (VAV, LBM), p. 762.

TACAS-2000-HermannsKMS #markov #model checking

A Markov Chain Model Checker (HH, JPK, JMK, MS), pp. 347–362.

AdaEurope-2000-CloshenH #ada #implementation #programming #using

An Ada95 Programming Style Checker Using the GNAT ASIS Implementation (PC, HJH), pp. 149–160.

CAV-2000-AbarbanelBGKW #automation #generative #named #simulation #specification

FoCs: Automatic Generation of Simulation Checkers from Formal Specifications (YA, IB, LG, SK, YW), pp. 538–542.

CAV-2000-Shtrichman #bound #model checking #satisfiability

Tuning SAT Checkers for Bounded Model Checking (OS), pp. 480–494.

LICS-2000-McMillan #model checking #proving #theorem

Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.

ICSE-1999-DangK #mobile #model checking #using

Using the ASTRAL Model Checker to Analyze Mobile IP (ZD, RAK), pp. 132–142.

DATE-1998-MetraFR

Highly Testable and Compact 1-out-of-n Code Checker with Single Output (CM, MF, BR), pp. 981–982.

TACAS-1998-Sprenger #calculus #coq #model checking #μ-calculus

A Verified Model Checker for the Modal μ-calculus in Coq (CS), pp. 167–183.

STOC-1998-ErgunKKRV

Spot-Checkers (FE, SK, RK, RR, MV), pp. 259–268.

FM-1998-FantechiGMPT #model checking

A Symbolic Model Checker for ACTL (AF, SG, FM, RP, ET), pp. 228–242.

CC-1998-LeinoN #static analysis

An Extended Static Checker for Modular-3 (KRML, GN), pp. 302–305.

CAV-1998-Holzmann #model checking #on the

On Checking Model Checkers (GJH), pp. 61–70.

DAC-1997-HasteerMB #performance

An Efficient Assertion Checker for Combinational Properties (GH, AM, PB), pp. 734–739.

FME-1997-YuL #implementation #model checking

Implementing a Model Checker for LEGO (SY, ZL), pp. 442–458.

CAV-1997-HenzingerHW #hybrid #model checking #named

HYTECH: A Model Checker for Hybrid Systems (TAH, PHH, HWT), pp. 460–463.

CAV-1997-Saidi #automation #deduction #invariant #verification

The Invariant Checker: Automated Deductive Verification of Reactive Systems (HS), pp. 436–439.

CAV-1997-SistlaMG #liveness #model checking #named #symmetry #verification

SMC: A Symmetry Based Model Checker for Verification of Liveness Properties (APS, LM, VG), pp. 464–467.

DAC-1996-Matsunaga #equivalence #performance

An Efficient Equivalence Checker for Combinational Circuits (YM), pp. 629–634.

CADE-1996-GiunchigliaV #abstraction #named #proving

ABSFOL: A Proof Checker with Abstraction (FG, AV), pp. 136–140.

ESEC-1995-TuyaSC #model checking #modelling #safety #using #verification

Using a Symbolic Model Checker for Verify Safety Properties in SA/RT Models (JT, LS, JAC), pp. 59–75.

CADE-1992-ChirimarGI #interface #named #performance #proving #visual notation

Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker (JC, CAG, MVI), pp. 711–715.

JICSLP-1992-RouzaudN #prolog #type system

Integrating Modes and Subtypes into a Prolog Type-Checker (YR, LNP), pp. 85–97.

ICALP-1991-KannanY #generative #probability

Program Checkers for Probability Generation (SK, ACCY), pp. 163–173.

VDME-1991-1-DammBH #consistency #editing

The VDM-SL Editor and Consistency Checker (FMD, HB, BSH), pp. 693–694.

ECOOP-1991-DelcourtZ #consistency #database #design #object-oriented

The Design of an Integrity Consistency Checker (ICC) for an Object-Oriented Database System (CD, RZ), pp. 97–117.

STOC-1990-Yao

Coherent Functions and Program Checkers (Extended Abstract) (ACCY), pp. 84–94.

CADE-1990-EichenlaubEHKP #proving

The Romulus Proof Checker (CE, BE, JH, CK, GP), pp. 651–652.

DAC-1984-KaneS #design

A systolic design rule checker (RK, SS), pp. 243–250.

DAC-1984-TaylorO #incremental

Magic’s incremental design-rule checker (GST, JKO), pp. 160–165.

CADE-1984-Ketonen #named #proving

EKL — A Mathematically Oriented Proof Checker (JK), pp. 65–79.

DAC-1983-TsukizoeSKF

MACH : a high-hitting pattern checker for VLSI mask data (AT, JS, TK, HF), pp. 726–731.

DAC-1979-McCaw

Unified Shapes Checker — a checking tool for LSI (CRM), pp. 81–87.

POPL-1977-SuzukiI #array #bound #implementation

Implementation of an Array Bound Checker (NS, KI), pp. 132–143.

DAC-1968-Baum

Printed circuit artwork checker (JDB).