BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Used together with:
model (103)
system (20)
use (20)
program (17)
specif (13)

Stem checker$ (all stems)

175 papers:

TACASTACAS-2015-CimattiGMT #hybrid #model checking #named #smt
HyComp: An SMT-Based Model Checker for Hybrid Systems (AC, AG, SM, ST), pp. 52–67.
FMFM-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.
OnwardOnward-2015-GreweEWM #performance #proving #type system
Type systems for the masses: deriving soundness proofs and efficient checkers (SG, SE, PW, MM), pp. 137–150.
SPLCSPLC-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.
CAVCAV-2015-MajumdarW #bound #model checking #named #source code
Bbs: A Phase-Bounded Model Checker for Asynchronous Programs (RM, ZW), pp. 496–503.
ICSTICST-2015-ZhangAC #exclamation #model checking #verification
Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications (HZ, TA, YC), pp. 1–10.
TACASTACAS-2014-ArmandoCC #model checking #named #satisfiability
SATMC: A SAT-Based Model Checker for Security-Critical Systems (AA, RC, LC), pp. 31–45.
TACASTACAS-2014-Gibson-RobinsonABR #csp #named #refinement
FDR3 — A Modern Refinement Checker for CSP (TGR, PJA, AB, AWR), pp. 187–201.
TACASTACAS-2014-KroeningT #bound #c #contest #model checking #named
CBMC — C Bounded Model Checker — (Competition Contribution) (DK, MT), pp. 389–391.
TACASTACAS-2014-MullerV #contest #named
CPAlien: Shape Analyzer for CPAChecker — (Competition Contribution) (PM, TV), pp. 395–397.
MSRMSR-2014-TulsianKKLN #algorithm #model checking #named
MUX: algorithm selection for software model checkers (VT, AK, RK, AL, AVN), pp. 132–141.
PLDIPLDI-2014-BiswasHSB #named #performance #precise
DoubleChecker: efficient sound and precise atomicity checking (SB, JH, AS, MDB), p. 6.
FMFM-2014-HahnLSTZ #model checking #named #probability
iscasMc: A Web-Based Probabilistic Model Checker (EMH, YL, SS, AT, LZ), pp. 312–317.
SEFMSEFM-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.
SEFMSEFM-2014-MotaFDW #agile #model checking #prototype #semantics
Rapid Prototyping of a Semantically Well Founded Circus Model Checker (AM, AF, AD, JW), pp. 235–249.
SEKESEKE-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.
FSEFSE-2014-LiYP0H #finite #infinity #ltl #named #satisfiability
Aalta: an LTL satisfiability checker over Infinite/Finite traces (JL, YY, GP, LZ, JH), pp. 731–734.
CGOCGO-2014-YanXYR #detection #memory management #named
LeakChecker: Practical Static Memory Leak Detection for Managed Languages (DY, G(X, SY, AR), p. 87.
CAVCAV-2014-CavadaCDGMMMRT #model checking
The nuXmv Symbolic Model Checker (RC, AC, MD, AG, AM, AM, SM, MR, ST), pp. 334–342.
CAVCAV-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.
ISSTAISSTA-2014-WeitzSKE #java #string
A format string checker for Java (KW, SS, GK, MDE), pp. 441–444.
ECSAECSA-2013-SilvaB #architecture #automation #consistency #named
PANDArch: A Pluggable Automated Non-intrusive Dynamic Architecture Conformance Checker (LdS, DB), pp. 240–248.
ASEASE-2013-FalkeMS #bound #model checking
The bounded model checker LLBMC (SF, FM, CS), pp. 706–709.
DACDAC-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.
TACASTACAS-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.
TACASTACAS-2013-FedyukovichSS #c #incremental #named
eVolCheck: Incremental Upgrade Checker for C (GF, OS, NS), pp. 292–307.
PEPMPEPM-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.
IFLIFL-2013-Protzenko #implementation
The implementation of the Mezzo type-checker (JP), p. 129.
SACSAC-2013-RenTSF #ruby
The ruby type checker (BMR, JT, TSS, JSF), pp. 1565–1572.
ESEC-FSEESEC-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.
ICSEICSE-2013-DongSL #model checking
Build your own model checker in one month (JSD, JS, YL), pp. 1481–1483.
CAVCAV-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.
CAVCAV-2013-ChengRS #constraints #named #polynomial
JBernstein: A Validity Checker for Generalized Polynomial Constraints (CHC, HR, NS), pp. 656–661.
CAVCAV-2013-EsparzaLNNSS #execution #ltl #model checking
A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.
ICSTICST-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.
ASEASE-2012-SongT #model checking #named #source code
PuMoC: a CTL model-checker for sequential programs (FS, TT), pp. 346–349.
DATEDATE-2012-MammoCPNZMB #approximate #simulation
Approximating checkers for simulation acceleration (BM, DC, DP, AN, AZ, RM, VB), pp. 153–158.
TACASTACAS-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.
SACSAC-2012-PerroneDH #graph #model checking
A model checker for Bigraphs (GP, SD, TTH), pp. 1320–1325.
CAVCAV-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.
CAVCAV-2012-HopkinsMO #equivalence #higher-order #ml #named
Hector: An Equivalence Checker for a Higher-Order Fragment of ML (DH, ASM, CHLO), pp. 774–780.
CAVCAV-2012-SongSLD #model checking #probability #realtime
A Model Checker for Hierarchical Probabilistic Real-Time Systems (SS, JS, YL, JSD), pp. 705–711.
ICSTICST-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.
ICALPICALP-v2-2011-ZhangB #model checking #probability
A Progress Measure for Explicit-State Probabilistic Model-Checkers (XZ, FvB), pp. 283–294.
ICSEICSE-2011-DietlDEMS #using
Building and using pluggable type-checkers (WD, SD, MDE, KM, TWS), pp. 681–690.
CAVCAV-2011-CimattiGMNR #model checking #named
Kratos — A Software Model Checker for SystemC (AC, AG, AM, IN, MR), pp. 310–316.
ICSTICST-2011-SaifanDBP #consistency #implementation #mobile #runtime
Implementing and Evaluating a Runtime Conformance Checker for Mobile Agent Systems (AAS, JD, JSB, EP), pp. 269–278.
DATEDATE-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.
DATEDATE-2010-GuglielmoFP #analysis
Vacuity analysis for property qualification by mutation of checkers (LDG, FF, GP), pp. 478–483.
TACASTACAS-2010-DragerKFW #concurrent #infinity #model checking #named
SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems (KD, AK, BF, HW), pp. 271–274.
WRLAWRLA-2010-BaeM #linear #logic #maude #model checking
The Linear Temporal Logic of Rewriting Maude Model Checker (KB, JM), pp. 208–225.
WRLAWRLA-2010-DuranM #equation #maude #order #specification
A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications (FD, JM), pp. 69–85.
WRLAWRLA-2010-DuranM10a #maude #order
A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories (FD, JM), pp. 86–103.
PLDIPLDI-2010-BurckhardtDMT #automation #named
Line-up: a complete and automatic linearizability checker (SB, CD, MM, RT), pp. 330–340.
SEFMSEFM-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.
LDTALDTA-2010-BrandMSH #case study #domain-specific language #experience
Formally specified type checkers for domain specific languages: experience report (MvdB, APvdM, AS, ATH), p. 12.
CAVCAV-2010-BozzanoCKNNRW #model checking
A Model Checker for AADL (MB, AC, JPK, VYN, TN, MR, RW), pp. 562–565.
CAVCAV-2010-Caniart #model checking #named
Merit: An Interpolating Model-Checker (NC), pp. 162–166.
CAVCAV-2010-HahnHWZ #markov #model checking #modelling #named #parametricity
PARAM: A Model Checker for Parametric Markov Models (EMH, HH, BW, LZ), pp. 660–664.
IJCARIJCAR-2010-GhilardiR #model checking #modulo theories #named
MCMT: A Model Checker Modulo Theories (SG, SR), pp. 22–29.
ESOPESOP-2009-SadowskiFF #named #parallel #source code #thread
SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs (CS, SNF, CF), pp. 394–409.
TACASTACAS-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.
CAVCAV-2009-HahnHWZ #infinity #markov #model checking #named
INFAMY: An Infinite-State Markov Model Checker (EMH, HH, BW, LZ), pp. 641–647.
CAVCAV-2009-HopkinsO #equivalence #higher-order #model checking #named
Homer: A Higher-Order Observational Equivalence Model checkER (DH, CHLO), pp. 654–660.
CAVCAV-2009-LomuscioQR #model checking #multi #named #verification
MCMAS: A Model Checker for the Verification of Multi-Agent Systems (AL, HQ, FR), pp. 682–688.
ICSTICST-2009-FraserG #evaluation #generative #model checking #specification #testing
An Evaluation of Model Checkers for Specification Based Test Case Generation (GF, AG), pp. 41–50.
QoSAQoSA-2008-PlsekA #component #model checking #named
Carmen: Software Component Model Checker (AP, JA), pp. 71–85.
ASEASE-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.
CSEETCSEET-2008-SalamahG #education #model checking #specification #using
A Technique for Using Model Checkers to Teach Formal Specifications (SS, AQG), pp. 181–188.
SCAMSCAM-2008-Cifuentes #c #debugging #named #scalability
Parfait — A Scalable Bug Checker for C Code (CC), pp. 263–264.
PLDIPLDI-2008-FlanaganFY #named #parallel #source code #thread
Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs (CF, SNF, JY), pp. 293–303.
ICSEICSE-2008-LongDG #experience #industrial #model checking
Experience applying the SPIN model checker to an industrial telecommunications system (BL, JD, TCNG), pp. 693–702.
OSDIOSDI-2008-GunawiRAA #declarative #file system #named
SQCK: A Declarative File System Checker (HSG, AR, ACAD, RHAD), pp. 131–146.
CAVCAV-2008-GayNP #model checking #named #quantum
QMC: A Model Checker for Quantum Systems (SJG, RN, NP), pp. 543–547.
IJCARIJCAR-2008-BoyerGJ #automaton
Certifying a Tree Automata Completion Checker (BB, TG, TPJ), pp. 523–538.
ASEASE-2007-KuHCL #benchmark #metric #model checking
A buffer overflow benchmark for software model checkers (KK, TEH, MC, DL), pp. 389–392.
ITiCSEITiCSE-2007-StallmannBRBGH #automaton #correctness #named #proving
ProofChecker: an accessible environment for automata theory correctness proofs (MFS, SB, RDR, SB, MCG, SDH), pp. 48–52.
FASEFASE-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.
SASSAS-2007-ChangRN #analysis #invariant
Shape Analysis with Structural Invariant Checkers (BYEC, XR, GCN), pp. 384–401.
IFMIFM-2007-PlaggeL #model checking #specification #using #validation
Validating Z Specifications Using the ProBAnimator and Model Checker (DP, ML), pp. 480–500.
ICFPICFP-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.
AMOSTAMOST-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.
MBTMBT-2007-BorodayPG #model checking #nondeterminism #question #testing
Can a Model Checker Generate Tests for Non-Deterministic Systems? (SB, AP, RG), pp. 3–19.
MBTMBT-2007-FraserAW #model checking #testing
Handling Model Changes: Regression Testing and Test-Suite Update with Model-Checkers (GF, BKA, FW), pp. 33–46.
MBTMBT-2007-RaimondiPB #model checking #testing
Testing Planning Domains (without Model Checkers) (FR, CP, GB), pp. 113–125.
ICSTSAT-2007-JussilaBSKW #proving #towards
A First Step Towards a Unified Proof Checker for QBF (TJ, AB, CS, DK, CMW), pp. 201–214.
ASEASE-2006-LiuYR #library #model checking #using
Software Library Usage Pattern Extraction Using a Software Model Checker (CL, EY, DJR), pp. 301–304.
DATEDATE-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.
TACASTACAS-2006-LomuscioR #model checking #multi #named
MCMAS: A Model Checker for Multi-agent Systems (AL, FR), pp. 450–454.
FMFM-2006-HuynhR #c# #memory management
A Memory Model Sensitive Checker for C# (TQH, AR), pp. 476–491.
QAPLQAPL-2005-KwiatkowskaNP06 #analysis #model checking #probability
Quantitative Analysis With the Probabilistic Model Checker PRISM (MZK, GN, DP), pp. 5–31.
PADLPADL-2006-Wang #automation #model checking #verification
Automatic Verification of a Model Checker by Reflection (BYW), pp. 45–59.
AMOSTAMOST-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.
CAVCAV-2006-GurfinkelWC #model checking #named #verification
Yasm: A Software Model-Checker for Verification and Refutation (AG, OW, MC), pp. 170–174.
CAVCAV-2006-SethiB #c #deduction #named
cascade: C Assertion Checker and Deductive Engine (NS, CB), pp. 166–169.
IJCARIJCAR-2006-HendrixMO #axiom #linear #order #specification
A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms (JH, JM, HO), pp. 151–155.
RTARTA-2006-WehrmanSW #named #termination
Slothrop: Knuth-Bendix Completion with a Modern Termination Checker (IW, AS, EMW), pp. 287–296.
WRLAWRLA-2004-PalominoP05 #maude #model checking #proving
Proving VLRL Action Properties with the Maude Model Checker (MP, IP), pp. 113–133.
ESOPESOP-2005-NaikP #model checking #type system
A Type System Equivalent to a Model Checker (MN, JP), pp. 374–388.
TACASTACAS-2005-SuwimonteerabuthSE #bytecode #java #named
jMoped: A Java Bytecode Checker Based on Moped (DS, SS, JE), pp. 541–545.
SEFMSEFM-2005-NivelleP #verification
Verification of an Off-Line Checker for Priority Queues (HdN, RP), pp. 210–219.
SEKESEKE-2005-Wang #infinity #logic #model checking #specification
Specification of an Infinite-State Local Model Checker in Rewriting Logic (BYW), pp. 442–447.
SACSAC-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.
AMOSTAMOST-2005-Robinson-MallettLMG #generative #model checking #sequence
Generating optimal distinguishing sequences with a model checker (CRM, PL, TM, UG).
CAVCAV-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.
CAVCAV-2005-Younes05a #model checking #named #statistics
Ymer: A Statistical Model Checker (HLSY), pp. 429–433.
TACASTACAS-2004-PiazzaPR #named #persistent #security
CoPS — Checker of Persistent Security (CP, EP, SR), pp. 144–152.
SEFMSEFM-2004-HamonMR #generative #model checking #performance #testing
Generating Efficient Test Sets with a Model Checker (GH, LMdM, JMR), pp. 261–270.
POPLPOPL-2004-FlanaganF #named #parallel #source code #thread
Atomizer: a dynamic atomicity checker for multithreaded programs (CF, SNF), pp. 256–267.
ICSEICSE-2004-GouldSD04a #sql #static analysis
JDBC Checker: A Static Analysis Tool for SQL/JDBC Applications (CG, ZS, PTD), pp. 697–698.
CAVCAV-2004-AndrewsQRRX #concurrent #model checking #named
Zing: A Model Checker for Concurrent Software (TA, SQ, SKR, JR, YX), pp. 484–487.
CAVCAV-2004-BarrettB #implementation
CVC Lite: A New Implementation of the Cooperating Validity Checker Category B (CWB, SB), pp. 515–518.
CAVCAV-2004-GriffaultV #model checking
The Mec 5 Model-Checker (AG, AV), pp. 488–491.
DACDAC-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.
DATEDATE-2003-OmanaRM #parallel
High Speed and Highly Testable Parallel Two-Rail Code Checker (MO, DR, CM), pp. 10608–10615.
DATEDATE-2003-Tarnick #embedded #self
Self-Testing Embedded Checkers for Bose-Lin, Bose, and a Class of Borden Codes (ST), pp. 11162–11163.
DATEDATE-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.
FMFME-2003-LeuschelB #model checking #named
ProB: A Model Checker for B (ML, MJB), pp. 855–874.
PPDPPPDP-2003-WuAS #proving
Foundational proof checkers with small witnesses (DW, AWA, AS), pp. 264–274.
ICSEICSE-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.
CAVCAV-2003-ChechikG #logic #named #query
TLQSolver: A Temporal Logic Query Checker (MC, AG), pp. 210–214.
FATESFATES-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.
VMCAIVMCAI-2003-CatanoH #ml #named #static analysis
CHASE: A Static Checker for JML’s Assignable Clause (NC, MH), pp. 26–40.
CBSECBSE-2003-Heineman #component #interface #modelling
Integrating Interface Assertion Checkers into Component Models (GTH), p. 9.
WRLAWRLA-2002-EkerMS #ltl #maude #model checking
The Maude LTL Model Checker (SE, JM, AS), pp. 162–187.
PASTEPASTE-2002-ChelfEH #how #static analysis
How to write system-specific, static checkers in metal (BC, DRE, SH), pp. 51–60.
FMFME-2002-HuberK #model checking #towards
Towards an Integrated Model Checker for Railway Signalling Data (MH, SK), pp. 204–223.
ICSEICSE-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.
CAVCAV-2002-ChechikGD #model checking #multi #named
chi-Chek: A Multi-valued Model-Checker (MC, AG, BD), pp. 505–509.
CAVCAV-2002-FlanaganQS #composition #parallel #source code #thread
A Modular Checker for Multithreaded Programs (CF, SQ, SAS), pp. 180–194.
CAVCAV-2002-GrocePY #adaptation #model checking #named
AMC: An Adaptive Model Checker (AG, DP, MY), pp. 521–525.
CAVCAV-2002-StumpBD #named
CVC: A Cooperating Validity Checker (AS, CWB, DLD), pp. 500–504.
SATSAT-2002-MalerMNA #difference #logic #satisfiability
A satisfiability checker for difference logic (OM, MM, PN, EA), p. 27.
TACASTACAS-2001-ChechikDE #implementation #model checking #multi
Implementing a Multi-valued Symbolic Model Checker (MC, BD, SME), pp. 404–419.
PADLPADL-2001-Kaser #generative #model checking
State Generation in the PARMC Model Checker (OK), pp. 337–352.
PADLPADL-2001-Ramakrishnan #calculus #logic programming #model checking #using #μ-calculus
A Model Checker for Value-Passing μ-Calculus Using Logic Programming (CRR), pp. 1–13.
CCCC-2001-MartenaP #alias #analysis #model checking
Alias Analysis by Means of a Model Checker (VM, PSP), pp. 3–19.
CAVCAV-2001-EsparzaS #model checking #recursion #source code
A BDD-Based Model Checker for Recursive Programs (JE, SS), pp. 324–336.
CAVCAV-2001-Namjoshi #model checking
Certifying Model Checkers (KSN), pp. 2–13.
CAVCAV-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.
DATEDATE-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.
TACASTACAS-2000-HermannsKMS #markov #model checking
A Markov Chain Model Checker (HH, JPK, JMK, MS), pp. 347–362.
AdaEuropeAdaEurope-2000-CloshenH #ada #implementation #programming #using
An Ada95 Programming Style Checker Using the GNAT ASIS Implementation (PC, HJH), pp. 149–160.
CAVCAV-2000-AbarbanelBGKW #automation #generative #named #simulation #specification
FoCs: Automatic Generation of Simulation Checkers from Formal Specifications (YA, IB, LG, SK, YW), pp. 538–542.
CAVCAV-2000-Shtrichman #bound #model checking #satisfiability
Tuning SAT Checkers for Bounded Model Checking (OS), pp. 480–494.
LICSLICS-2000-McMillan #model checking #proving #theorem
Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.
ICSEICSE-1999-DangK #mobile #model checking #using
Using the ASTRAL Model Checker to Analyze Mobile IP (ZD, RAK), pp. 132–142.
DATEDATE-1998-MetraFR
Highly Testable and Compact 1-out-of-n Code Checker with Single Output (CM, MF, BR), pp. 981–982.
TACASTACAS-1998-Sprenger #calculus #coq #model checking #μ-calculus
A Verified Model Checker for the Modal μ-calculus in Coq (CS), pp. 167–183.
STOCSTOC-1998-ErgunKKRV
Spot-Checkers (FE, SK, RK, RR, MV), pp. 259–268.
FMFM-1998-FantechiGMPT #model checking
A Symbolic Model Checker for ACTL (AF, SG, FM, RP, ET), pp. 228–242.
CCCC-1998-LeinoN #static analysis
An Extended Static Checker for Modular-3 (KRML, GN), pp. 302–305.
CAVCAV-1998-Holzmann #model checking #on the
On Checking Model Checkers (GJH), pp. 61–70.
DACDAC-1997-HasteerMB #performance
An Efficient Assertion Checker for Combinational Properties (GH, AM, PB), pp. 734–739.
FMFME-1997-YuL #implementation #model checking
Implementing a Model Checker for LEGO (SY, ZL), pp. 442–458.
CAVCAV-1997-HenzingerHW #hybrid #model checking #named
HYTECH: A Model Checker for Hybrid Systems (TAH, PHH, HWT), pp. 460–463.
CAVCAV-1997-Saidi #automation #deduction #invariant #verification
The Invariant Checker: Automated Deductive Verification of Reactive Systems (HS), pp. 436–439.
CAVCAV-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.
DACDAC-1996-Matsunaga #equivalence #performance
An Efficient Equivalence Checker for Combinational Circuits (YM), pp. 629–634.
CADECADE-1996-GiunchigliaV #abstraction #named #proving
ABSFOL: A Proof Checker with Abstraction (FG, AV), pp. 136–140.
ESECESEC-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.
CADECADE-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.
ICLPJICSLP-1992-RouzaudN #prolog #type system
Integrating Modes and Subtypes into a Prolog Type-Checker (YR, LNP), pp. 85–97.
ICALPICALP-1991-KannanY #generative #probability
Program Checkers for Probability Generation (SK, ACCY), pp. 163–173.
FMVDME-1991-1-DammBH #consistency #editing
The VDM-SL Editor and Consistency Checker (FMD, HB, BSH), pp. 693–694.
ECOOPECOOP-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.
STOCSTOC-1990-Yao
Coherent Functions and Program Checkers (Extended Abstract) (ACCY), pp. 84–94.
CADECADE-1990-EichenlaubEHKP #proving
The Romulus Proof Checker (CE, BE, JH, CK, GP), pp. 651–652.
DACDAC-1984-KaneS #design
A systolic design rule checker (RK, SS), pp. 243–250.
DACDAC-1984-TaylorO #incremental
Magic’s incremental design-rule checker (GST, JKO), pp. 160–165.
CADECADE-1984-Ketonen #named #proving
EKL — A Mathematically Oriented Proof Checker (JK), pp. 65–79.
DACDAC-1983-TsukizoeSKF
MACH : a high-hitting pattern checker for VLSI mask data (AT, JS, TK, HF), pp. 726–731.
DACDAC-1979-McCaw
Unified Shapes Checker — a checking tool for LSI (CRM), pp. 81–87.
POPLPOPL-1977-SuzukiI #array #bound #implementation
Implementation of an Array Bound Checker (NS, KI), pp. 132–143.
DACDAC-1968-Baum
Printed circuit artwork checker (JDB).

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.