BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
model checking
Google model checking

Tag #model checking

1111 papers:

ASPLOSASPLOS-2020-Kokologiannakis #hardware #memory management #modelling #named
HMC: Model Checking for Hardware Memory Models (MK, VV), pp. 1157–1171.
FMFM-2019-Ehlers #how #question
How Hard Is Finding Shortest Counter-Example Lassos in Model Checking? (RE), pp. 245–261.
FMFM-2019-GomesB #towards
Towards a Model-Checker for Circus (AOG, AB), pp. 217–234.
FMFM-2019-GomesB19a #csp #named #using
Circus2CSP: A Tool for Model-Checking Circus Using FDR (AOG, AB), pp. 235–242.
FMFM-2019-KwiatkowskaN0S #concurrent #game studies #probability
Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games (MK, GN, DP0, GS), pp. 298–315.
FSCDFSCD-2019-RubioMPV #term rewriting
Model Checking Strategy-Controlled Rewriting Systems (System Description) (RR, NMO, IP, AV), p. 18.
IFM-2019-CoullonJL #design #distributed #performance
Integrated Model-Checking for the Design of Safe and Efficient Distributed Software Commissioning (HC, CJ, DL), pp. 120–137.
IFM-2019-DubslaffKT #probability
Ontology-Mediated Probabilistic Model Checking (CD, PK, AYT), pp. 194–211.
OOPSLAOOPSLA-2019-AbdullaAJLNS #consistency #equivalence
Optimal stateless model checking for reads-from equivalence under sequential consistency (PAA, MFA, BJ, ML, TPN, KS), p. 29.
OOPSLAOOPSLA-2019-Kokologiannakis #effectiveness
Effective lock handling in stateless model checking (MK, AR, VV), p. 26.
OOPSLAOOPSLA-2019-KonnovKT
TLA+ model checking made symbolic (IK, JK, THT), p. 30.
PEPMPEPM-2019-SatoI0 #higher-order #refinement #type inference
Combining higher-order model checking with refinement type inference (RS, NI, NK0), pp. 47–53.
PLDIPLDI-2019-Kokologiannakis #consistency #library
Model checking for weakly consistent libraries (MK, AR, VV), pp. 96–110.
POPLPOPL-2019-BaeL #bound #logic #using
Bounded model checking of signal temporal logic properties using syntactic separation (KB, JL), p. 30.
PPDPPPDP-2019-Kobayashi #higher-order
10 Years of the Higher-Order Model Checking Project (Extended Abstract) (NK0), p. 2.
ASEASE-2019-KimC #embedded #using
Model Checking Embedded Control Software using OS-in-the-Loop CEGAR (DK, YC), pp. 565–576.
ESEC-FSEESEC-FSE-2019-LangP #c++ #case study #framework
Model checking a C++ software framework: a case study (JL, ISWBP), pp. 1026–1036.
ESEC-FSEESEC-FSE-2019-NejatiGMBFW #modelling #requirements #testing
Evaluating model testing and model checking for finding requirements violations in Simulink models (SN, KG, CM, LCB, SF, DW), pp. 1015–1025.
ESEC-FSEESEC-FSE-2019-ZhangSYZPS #comprehension #debugging
Finding and understanding bugs in software model checkers (CZ, TS, YY, FZ, GP, ZS), pp. 763–773.
FASEFASE-2019-DimovskiLW #abstraction #game studies #refinement #variability
Variability Abstraction and Refinement for Game-Based Lifted Model Checking of Full CTL (ASD, AL, AW), pp. 192–209.
CAVCAV-2019-AshokKW #game studies #markov #probability #process #statistics
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games (PA, JK, MW), pp. 497–519.
CAVCAV-2019-NeupaneMM00 #analysis #approximate #infinity #named #probability
STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis (TN, CJM, CM, HZ0, ZZ0), pp. 540–549.
ICTSSICTSS-2019-VinarskiiLKYZ #approach #detection
A Model Checking Based Approach for Detecting SDN Races (EV, JL, NK, NY, DZ), pp. 194–211.
VMCAIVMCAI-2019-AndreFMS #abstraction #algorithm #industrial #parametricity #using #verification
Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking (ÉA, LF, JMM, RS), pp. 409–424.
VMCAIVMCAI-2019-BuenoS #named
euforia: Complete Software Model Checking with Uninterpreted Functions (DB, KAS), pp. 363–385.
VMCAIVMCAI-2019-DeckerP #ltl #quantifier #using
Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic (ND, AP), pp. 513–534.
FMFM-2018-GeislerH #development #distributed #using
Stepwise Development and Model Checking of a Distributed Interlocking System - Using RAISE (SG, AEH), pp. 277–293.
FMFM-2018-LegayNPT #statistics
Statistical Model Checking of LLVM Code (AL, DN, DBP, LMT), pp. 542–549.
IFM-2018-KornerLM #state of the art #using
State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin (PK, ML, JM), pp. 275–295.
OOPSLAOOPSLA-2018-AbdullaAJN #semantics
Optimal stateless model checking under the release-acquire semantics (PAA, MFA, BJ, TPN), p. 29.
POPLPOPL-2018-Kokologiannakis #c #c++ #concurrent #effectiveness
Effective stateless model checking for C/C++ concurrency (MK, OL, KS, VV), p. 32.
ASEASE-2018-BeyerF #concurrent #independence #multi #thread
Domain-independent multi-threaded software model checking (DB, KF), pp. 634–644.
ASEASE-2018-BrunelCCM #first-order #relational #specification
The electrum analyzer: model checking relational first-order temporal specifications (JB, DC, AC, NM), pp. 884–887.
ASEASE-2018-GadelhaMMC0N #c
ESBMC 5.0: an industrial-strength C model checker (MYRG, FRM, JM, LCC, BF0, DAN), pp. 888–891.
ASEASE-2018-MonteiroGCF #bound #c++ #framework #platform #source code
Bounded model checking of C++ programs based on the Qt cross-platform framework (journal-first abstract) (FRM, MAPG, LCC, EBdLF), p. 954.
ASEASE-2018-WangCYJ #analysis #approach #constraints #string
A symbolic model checking approach to the analysis of string and length constraints (HEW, SYC, FY, JHRJ), pp. 623–633.
ESEC-FSEESEC-FSE-2018-Anand #distributed #hybrid #named
Dara: hybrid model checking of distributed systems (VA), pp. 977–979.
ESOPESOP-2018-0001TW #higher-order #verification
Higher-Order Program Verification via HFL Model Checking (NK0, TT, KW), pp. 711–738.
FASEFASE-2018-Dimovski #using
Abstract Family-Based Model Checking Using Modal Featured Transition Systems: Preservation of CTL* (ASD), pp. 301–318.
CAVCAV-2018-CordeiroKKST #bound #bytecode #java #named #verification
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (LCC, PK, DK, PS, MT), pp. 183–190.
CAVCAV-2018-FinkbeinerHT
Model Checking Quantitative Hyperproperties (BF, CH, HT), pp. 144–163.
CAVCAV-2018-McMillan #abstraction
Eager Abstraction for Symbolic Model Checking (KLM), pp. 191–208.
CAVCAV-2018-BauerCS0 #protocol #random #security
Model Checking Indistinguishability of Randomized Security Protocols (MSB, RC, APS, MV0), pp. 117–135.
CAVCAV-2018-CookKKTTT
Model Checking Boot Code from AWS Data Centers (BC, KK, DK, ST, MT, MRT), pp. 467–486.
CAVCAV-2018-GacekBWWG
The JKind Model Checker (AG, JB, MW, LGW, EG), pp. 20–27.
IJCARIJCAR-2018-ConchonDZ #memory management
Cubicle- W : Parameterized Model Checking on Weak Memory (SC, DD, FZ), pp. 152–160.
VMCAIVMCAI-2018-AminofRSWZ #abstraction #algorithm #distributed
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction (BA, SR, IS, JW, FZ), pp. 1–24.
VMCAIVMCAI-2018-BruniGG #obfuscation
Code Obfuscation Against Abstract Model Checking Attacks (RB, RG, RG), pp. 94–115.
VMCAIVMCAI-2018-SchindlerJ #infinity
Selfless Interpolation for Infinite-State Model Checking (TS, DJ), pp. 495–515.
FSCDFSCD-2017-SuzukiF0T #automaton #higher-order #recursion
Streett Automata Model Checking of Higher-Order Recursion Schemes (RS0, KF, NK0, TT), p. 18.
IFM-2017-AronisFS #testing #using #verification
Testing and Verifying Chain Repair Methods for Corfu Using Stateless Model Checking (SA, SLF, KS), pp. 227–242.
IFM-2017-BruschiPGLP #case study #protocol #smt #verification
Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study - (DB, ADP, SG, AL, EP), pp. 391–406.
SEFMSEFM-2017-BernasconiMSZG #modelling #proving
From Model Checking to a Temporal Proof for Partial Models (AB0, CM, PS, LDZ, CG), pp. 54–69.
SEFMSEFM-2017-BozzelliMMP #logic #regular expression
An In-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions (LB, AM, AM, AP), pp. 104–119.
SEFMSEFM-2017-CabodiCPPV #bound #learning
Interpolation-Based Learning as a Mean to Speed-Up Bounded Model Checking (Short Paper) (GC, PC, MP, PP, DV), pp. 382–387.
OOPSLAOOPSLA-2017-UgawaAM #concurrent #garbage collection #memory management #modelling
Model checking copy phases of concurrent copying garbage collection with various memory models (TU, TA0, TM), p. 26.
PEPMPEPM-2017-SuwaT0I #code generation #higher-order #verification
Verification of code generators via higher-order model checking (TS, TT, NK0, AI), pp. 59–70.
ASEASE-2017-CastanoBGU #execution
Model checker execution reports (RC, VAB, DG, SU), pp. 200–205.
ASEASE-2017-TianDDO #effectiveness
More effective interpolations in software model checking (CT, ZD, ZD, CHLO), pp. 183–193.
ESEC-FSEESEC-FSE-2017-DietschHMNP
Craig vs. Newton in software model checking (DD, MH, BM, AN, AP), pp. 487–497.
ESEC-FSEESEC-FSE-2017-LlerenaSR #in the cloud #probability
Probabilistic model checking of perturbed MDPs with applications to cloud computing (YRSL, GS, DSR), pp. 454–464.
FASEFASE-2017-BeekVW
Family-Based Model Checking with mCRL2 (MHtB, EPdV, TACW), pp. 387–405.
FASEFASE-2017-DimovskiW #abstraction #refinement #variability
Variability-Specific Abstraction Refinement for Family-Based Model Checking (ASD, AW), pp. 406–423.
FASEFASE-2017-Wang0YP #approach #empirical #modelling #probability
Should We Learn Probabilistic Models for Model Checking? A New Approach and An Empirical Study (JW, JS0, QY, JP0), pp. 3–21.
CAVCAV-2017-Baier0L0W #markov #process #reliability
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes (CB, JK0, LL, DP0, SW), pp. 160–180.
CAVCAV-2017-WijsN #composition #incremental
Compositional Model Checking with Incremental Counter-Example Construction (AW, TN), pp. 570–590.
CAVCAV-2017-DehnertJK0 #probability
A Storm is Coming: A Modern Probabilistic Model Checker (CD, SJ, JPK, MV0), pp. 592–600.
CAVCAV-2017-FortinMW #automaton #linear
Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems (MF, AM, IW), pp. 155–175.
CSLCSL-2017-Kreutzer #first-order #roadmap
Current Trends and New Perspectives for First-Order Model Checking (Invited Talk) (SK), p. 5.
ICSTICST-2017-AichernigS #statistics #testing
Statistical Model Checking Meets Property-Based Testing (BKA, RS), pp. 390–400.
ICSTICST-2017-ArcainiGR17a #framework #named
NuSeen: A Tool Framework for the NuSMV Model Checker (PA, AG, ER), pp. 476–483.
ICSTICST-2017-DarkeCCV #abstraction #bound #performance #proving #safety #using
Efficient Safety Proofs for Industry-Scale Code Using Abstractions and Bounded Model Checking (PD, BC, AC, RV), pp. 468–475.
ICSTICST-2017-MilewiczP #named #static analysis
Ariadne: Hybridizing Directed Model Checking and Static Analysis (RM, PP), pp. 442–447.
ICTSSICTSS-2017-KrafczykP #clustering #effectiveness #equivalence #infinity
Effective Infinite-State Model Checking by Input Equivalence Class Partitioning (NK, JP0), pp. 38–53.
VMCAIVMCAI-2017-AhmedBBDFHINPRS #ltl
Bringing LTL Model Checking to Biologists (ZA, DB, SB, ACED, JF, BAH, SI, JN, NP, MR, NS), pp. 1–13.
VMCAIVMCAI-2017-GuntherLSW #concurrent #reduction
Dynamic Reductions for Model Checking Concurrent Software (HG, AL, AS, GW), pp. 246–265.
ECSAECSA-2016-CavalcanteQTOBL #architecture #statistics
Statistical Model Checking of Dynamic Software Architectures (EC, JQ, LMT, FO, TB, AL), pp. 185–200.
SCAMSCAM-2016-GaoHMW #bound #named #testing
LLSPLAT: Improving Concolic Testing by Bounded Model Checking (MG0, LH, RM, ZW), pp. 127–136.
FMFM-2016-BenesBDPS #analysis #approach
A Model Checking Approach to Discrete Bifurcation Analysis (NB, LB, MD, SP, DS), pp. 85–101.
FMFM-2016-FilipovikjMMSLL #industrial #statistics
Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems (PF, NM, RM, CS, OL, HL), pp. 748–756.
FMFM-2016-MenghiSG
Dealing with Incompleteness in Automata-Based Model Checking (CM, PS, CG), pp. 531–550.
FMFM-2016-WijsNB #gpu
GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking (AW, TN, DB), pp. 694–701.
SEFMSEFM-2016-DobrikovLP #ltl
LTL Model Checking under Fairness in ProB (ID, ML, DP), pp. 204–211.
SEFMSEFM-2016-HusienS #generative #using
Program Generation Using Simulated Annealing and Model Checking (IH, SS), pp. 155–171.
SEFMSEFM-2016-Smith #simulation
Model Checking Simulation Rules for Linearizability (GS), pp. 188–203.
OOPSLAOOPSLA-2016-BlumG
Stateless model checking with data-race preemption points (BB, GAG), pp. 477–493.
AdaEuropeAdaEurope-2016-Mazzanti #ada #experience #manycore #parallel #programming
An Experience in Ada Multicore Programming: Parallelisation of a Model Checking Engine (FM), pp. 94–109.
LOPSTRLOPSTR-2016-JanaKDVC #array #bound #scalability #source code
Scaling Bounded Model Checking by Transforming Programs with Arrays (AJ, UPK, AD, RV, NC), pp. 275–292.
POPLPOPL-2016-BrotherstonGKR #induction #logic
Model checking for symbolic-heap separation logic with inductive predicates (JB, NG, MIK, RR), pp. 84–96.
POPLPOPL-2016-HasuoSC #algebra #metric
Lattice-theoretic progress measures and coalgebraic model checking (IH, SS, CC), pp. 718–732.
ASEASE-2016-Nishi #bound #programming #towards #using
Towards bounded model checking using nonlinear programming solver (MN), pp. 560–565.
FSEFSE-2016-Apel0MMS #composition #on the fly #specification
On-the-fly decomposition of specifications in software model checking (SA, DB0, VOM, VSM, AS), pp. 349–361.
FSEFSE-2016-Monteiro #bound #finite #fixpoint #implementation #modelling
Bounded model checking of state-space digital systems: the impact of finite word-length effects on the implementation of fixed-point digital controllers based on state-space modeling (FRM), pp. 1151–1153.
ICSE-2016-SuRT #evaluation #parametricity #reliability #runtime #using
Reliability of Run-Time Quality-of-Service evaluation using parametric model checking (GS, DSR, GT), pp. 73–84.
CASECASE-2016-TsukadaSS #composition
A toolchain on model checking SPIN via Kalman Decomposition for control system software (KT, KS, SS), pp. 300–305.
FASEFASE-2016-DuranMA #domain-specific language #modelling #statistics
Statistical Model Checking of e-Motions Domain-Specific Modeling Languages (FD, AMD, JMÁP), pp. 305–322.
CAVCAV-2016-AbdullaAJL
Stateless Model Checking for POWER (PAA, MFA, BJ, CL), pp. 134–156.
CAVCAV-2016-ChampionMST
The Kind 2 Model Checker (AC, AM, CS, CT), pp. 510–517.
CAVCAV-2016-Fiterau-Brostean #implementation #learning
Combining Model Learning and Model Checking to Analyze TCP Implementations (PFB, RJ, FWV), pp. 454–471.
CAVCAV-2016-GarioCMTR #automation #design #scalability
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration (MG, AC, CM, ST, KYR), pp. 3–22.
CAVCAV-2016-Wijs #linear
BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs (AW), pp. 472–493.
ICSTICST-2016-GhafoorMS #database #effectiveness #partial order #reduction
Effective Partial Order Reduction in Model Checking Database Applications (MAG, MSM, JHS), pp. 146–156.
ICTSSICTSS-2016-EnoiuSCFP #embedded #generative #testing #using
Mutation-Based Test Generation for PLC Embedded Software Using Model Checking (EPE, DS, AC, RF, PP), pp. 155–171.
IJCARIJCAR-2016-AminofR #composition #multi
Model Checking Parameterised Multi-token Systems via the Composition Method (BA, SR), pp. 499–515.
IJCARIJCAR-2016-BozzelliMMPS #logic
Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments (LB, AM, AM, AP, PS), pp. 389–405.
TAPTAP-2016-GabmeyerS #graph transformation #hardware #lightweight #off the shelf #verification
Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers (SG, MS), pp. 94–111.
VMCAIVMCAI-2016-ChakiK #concurrent #multi #thread
Model Checking with Multi-threaded IC3 Portfolios (SC, DK), pp. 517–535.
SANERSANER-2015-NayrollesHTL #approach #debugging #named #using
JCHARMING: A bug reproduction approach using crash traces and directed model checking (MN, AHL, ST, AL), pp. 101–110.
LATALATA-2015-Salem #automaton #ltl #testing
Single-Pass Testing Automata for LTL Model Checking (AEBS), pp. 563–576.
FMFM-2015-0001K #bound #using
Property-Driven Fence Insertion Using Reorder Bounded Model Checking (SJ, DK), pp. 291–307.
FMFM-2015-ChimdyalwarDCVC #abstraction #bound #static analysis #using
Eliminating Static Analysis False Positives Using Loop Abstraction and Bounded Model Checking (BC, PD, AC, SV, AC), pp. 573–576.
FMFM-2015-ConchonMZ
Certificates for Parameterized Model Checking (SC, AM, FZ), pp. 126–142.
FMFM-2015-FengHTZ #named #protocol #quantum #source code
QPMC: A Model Checker for Quantum Programs and Protocols (YF, EMH, AT, LZ), pp. 265–272.
FMFM-2015-KroeningLW #automaton #bound #proving #safety
Proving Safety with Trace Automata and Bounded Model Checking (DK, ML, GW), pp. 325–341.
FMFM-2015-ZhuYGZZZ #data flow #graph #scheduling
Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking (XZ, RY, YLG, JZ, WZ, GZ), pp. 551–569.
SEFMSEFM-2015-RochaBC #bound #c #generative #memory management #source code #testing #using
Memory Management Test-Case Generation of C Programs Using Bounded Model Checking (HR, RSB, LCC), pp. 251–267.
SEFMSEFM-2015-RockaiSB #c #c++
Techniques for Memory-Efficient Model Checking of C and C++ Code (PR, VS, JB), pp. 268–282.
SPLCSPLC-2015-DimovskiABW #off the shelf #using
Family-based model checking using off-the-shelf model checkers: extended abstract (ASD, ASAS, CB, AW), p. 397.
OOPSLAOOPSLA-2015-DemskyL #named
SATCheck: SAT-directed stateless model checking for SC and TSO (BD, PL), pp. 20–36.
OOPSLAOOPSLA-2015-JensenMRDV
Stateless model checking of event-driven applications (CSJ, AM, VR, DD, MTV), pp. 57–73.
PLDIPLDI-2015-Huang #concurrent #reduction #source code
Stateless model checking concurrent programs with maximal causality reduction (JH), pp. 165–174.
ASEASE-2015-InversoN0TP #bound #concurrent #multi #named #thread
Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs (OI, TLN, BF, SLT, GP), pp. 807–812.
ASEASE-2015-MercerAVS #parallel #source code #using
Model Checking Task Parallel Programs Using Gradual Permissions (N) (EGM, PA, NV, VS), pp. 535–540.
ESEC-FSEESEC-FSE-2015-MorenoCGS #adaptation #approach #nondeterminism #probability #self
Proactive self-adaptation under uncertainty: a probabilistic model checking approach (GAM, JC, DG, BRS), pp. 1–12.
ICSEICSE-v1-2015-Ben-DavidSAB #product line #requirements #satisfiability #using
Symbolic Model Checking of Product-Line Requirements Using SAT-Based Methods (SBD, BS, JMA, SB), pp. 189–199.
ICSEICSE-v1-2015-SuFPHS #data flow #execution #symbolic computation #testing
Combining Symbolic Execution and Model Checking for Data Flow Testing (TS, ZF, GP, JH, ZS), pp. 654–665.
SACSAC-2015-CamaraGS0 #adaptation #architecture #game studies #probability #self
Optimal planning for architecture-based self-adaptation via model checking of stochastic games (JC, DG, BRS, AP), pp. 428–435.
SACSAC-2015-DiazCMR #architecture #verification #web #web service
Model-checking verification of publish-subscribe architectures in web service contexts (GD, MEC, HM, VVR), pp. 1688–1695.
DACDAC-2015-MundhenkSLFC #analysis #architecture #probability #security #using
Security analysis of automotive architectures using probabilistic model checking (PM, SS, ML, SAF, SC), p. 6.
DATEDATE-2015-ChangD #analysis #modelling #using
May-happen-in-parallel analysis of ESL models using UPPAAL model checking (CWC, RD), pp. 1567–1570.
DATEDATE-2015-ChenYQFM #evaluation #scheduling #statistics #using
Variation-aware evaluation of MPSoC task allocation and scheduling strategies using statistical model checking (MC, DY, XQ, XF, PM), pp. 199–204.
DATEDATE-2015-DarkeCVSM #approximate #bound #using
Over-approximating loops to prove properties using bounded model checking (PD, BC, RV, US, RM), pp. 1407–1412.
DATEDATE-2015-HoqueMS #analysis #approach #maintenance #probability #reliability #towards
Towards an accurate reliability, availability and maintainability analysis approach for satellite systems based on probabilistic model checking (KAH, OAM, YS), pp. 1635–1640.
FASEFASE-2015-FedyukovichDHS #bound #dependence #detection
Symbolic Detection of Assertion Dependencies for Bounded Model Checking (GF, ACD, AEJH, NS), pp. 186–201.
TACASTACAS-2015-AbdullaAAJLS
Stateless Model Checking for TSO and PSO (PAA, SA, MFA, BJ, CL, KFS), pp. 353–367.
TACASTACAS-2015-CimattiGMT #hybrid #named #smt
HyComp: An SMT-Based Model Checker for Hybrid Systems (AC, AG, SM, ST), pp. 52–67.
TACASTACAS-2015-GiacobbeGGHPP #network
Model Checking Gene Regulatory Networks (MG, CCG, AG, TAH, TP, TP), pp. 469–483.
TACASTACAS-2015-HansenWCNK #semantics #statistics
Semantic Importance Sampling for Statistical Model Checking (JPH, LW, SC, DdN, MHK), pp. 241–255.
TACASTACAS-2015-KantLMPBD #independence #named
LTSmin: High-Performance Language-Independent Model Checking (GK, AL, JM, JvdP, SB, TvD), pp. 692–707.
TACASTACAS-2015-MolnarDVB #incremental #induction #ltl #proving
Saturation-Based Incremental LTL Model Checking with Inductive Proofs (VM, DD, AV, TB), pp. 643–657.
TACASTACAS-2015-RenaultDKP #automaton #parallel
Parallel Explicit Model Checking for Generalized Büchi Automata (ER, ADL, FK, DP), pp. 613–627.
TACASTACAS-2015-Thierry-Mieg #using
Symbolic Model-Checking Using ITS-Tools (YTM), pp. 231–237.
CADECADE-2015-Ji #deduction
CTL Model Checking in Deduction Modulo (KJ), pp. 295–310.
CAVCAV-2015-DietschHLP #approach #ltl #modulo theories
Fairness Modulo Theory: A New Approach to LTL Software Model Checking (DD, MH, VL, AP), pp. 49–66.
CAVCAV-2015-Durand-Gasselin
Model Checking Parameterized Asynchronous Shared-Memory Systems (ADG, JE, PG, RM), pp. 67–84.
CAVCAV-2015-FinkbeinerRS #algorithm
Algorithms for Model Checking HyperLTL and HyperCTL ^* (BF, MNR, CS), pp. 30–48.
CAVCAV-2015-KonnovVW #abstraction #algorithm #distributed #smt
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms (IK, HV, JW), pp. 85–102.
CAVCAV-2015-MajumdarW #bound #named #source code
Bbs: A Phase-Bounded Model Checker for Asynchronous Programs (RM, ZW), pp. 496–503.
CSLCSL-2015-GrelloisM #higher-order #linear #logic #relational #semantics
Relational Semantics of Linear Logic and Higher-order Model Checking (CG, PAM), pp. 260–276.
CSLCSL-2015-MolinariMP #logic
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives (AM, AM, AP), pp. 193–210.
ICSTICST-2015-ZhangAC #exclamation #verification
Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications (HZ, TA, YC), pp. 1–10.
LICSLICS-2015-KobayashiL #abstraction #refinement
Automata-Based Abstraction Refinement for μHORS Model Checking (NK, XL), pp. 713–724.
LICSLICS-2015-Ong #higher-order #overview #perspective
Higher-Order Model Checking: An Overview (LO), pp. 1–15.
CBSECBSE-2014-MateescuSY #parallel #process #using
Quantifying the parallelism in BPMN processes using model checking (RM, GS, LY), pp. 159–168.
MSRMSR-2014-TulsianKKLN #algorithm #named
MUX: algorithm selection for software model checkers (VT, AK, RK, AL, AVN), pp. 132–141.
AFLAFL-2014-CarayolH #algorithm #automaton
Saturation algorithms for model-checking pushdown systems (AC, MH), pp. 1–24.
LATALATA-2014-KleinMBK #automaton #probability #question
Are Good-for-Games Automata Good for Probabilistic Model Checking? (JK, DM, CB, SK), pp. 453–465.
FMFM-2014-BaiHWLLM #formal method #named #platform #towards
TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms (GB, JH, JW, YL, ZL, AM), pp. 110–126.
FMFM-2014-HahnLSTZ #named #probability
iscasMc: A Web-Based Probabilistic Model Checker (EMH, YL, SS, AT, LZ), pp. 312–317.
FMFM-2014-LinH #composition #concurrent #learning #synthesis
Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning (SWL, PAH), pp. 416–431.
IFMIFM-2014-OliveiraSF #specification
Model-Checking Circus State-Rich Specifications (MVMO, ACAS, MSCF), pp. 39–54.
SEFMSEFM-2014-DobrikovL #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 #prototype #semantics
Rapid Prototyping of a Semantically Well Founded Circus Model Checker (AM, AF, AD, JW), pp. 235–249.
SFMSFM-2014-GmeinerKSVW #algorithm #distributed #fault tolerance #tutorial
Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms (AG, IK, US, HV, JW), pp. 122–171.
ICGTICGT-2014-Delzanno #distributed #protocol #verification
Parameterized Verification and Model Checking for Distributed Broadcast Protocols (GD), pp. 1–16.
KRKR-2014-LomuscioM14a #bound
Model Checking Unbounded Artifact-Centric Systems (AL, JM).
SPLCSPLC-2014-ThumMBHRS #product line #proving #theorem proving
Potential synergies of theorem proving and model checking for software product lines (TT, JM, FB, MH, AvR, GS), pp. 177–186.
HILTHILT-2014-RathjeR #framework #java #network #source code
A framework for model checking UDP network programs with Java pathfinder (WR, BR), pp. 81–86.
POPLPOPL-2014-RamsayNO #abstraction #approach #higher-order #refinement
A type-directed abstraction refinement approach to higher-order model checking (SJR, RPN, CHLO), pp. 61–72.
QAPLQAPL-2014-SpielerHZ #markov #modelling
Model Checking CSL for Markov Population Models (DS, EMH, LZ), pp. 93–107.
FSEFSE-2014-Kan #safety #traceability #verification
Traceability and model checking to support safety requirement verification (SK), pp. 783–786.
SLESLE-2014-BillGKS #ocl #specification
Model Checking of CTL-Extended OCL Specifications (RB, SG, PK, MS), pp. 221–240.
OSDIOSDI-2014-LeesatapornwongsaHJLG #debugging #named #performance #semantics
SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems (TL, MH, PJ, JFL, HSG), pp. 399–414.
PDPPDP-2014-BarnatBH #parallel #source code
Model Checking Parallel Programs with Inputs (JB, PB, VH), pp. 756–759.
FASEFASE-2014-BaierDKDKMW #multi #probability #reasoning #standard
Probabilistic Model Checking and Non-standard Multi-objective Reasoning (CB, CD, SK, MD, JK, SM, SW), pp. 1–16.
FoSSaCSFoSSaCS-2014-Tsukada0 #call-by #complexity #source code
Complexity of Model-Checking Call-by-Value Programs (TT, NK), pp. 180–194.
TACASTACAS-2014-ArmandoCC #named #satisfiability
SATMC: A SAT-Based Model Checker for Security-Critical Systems (AA, RC, LC), pp. 31–45.
TACASTACAS-2014-KroeningT #bound #c #contest #named
CBMC — C Bounded Model Checker — (Competition Contribution) (DK, MT), pp. 389–391.
TACASTACAS-2014-SalemDKT #automaton #invariant #testing #using
Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata (AEBS, ADL, FK, YTM), pp. 440–454.
WRLAWRLA-2014-BaeM #infinity #using
Infinite-State Model Checking of LTLR Formulas Using Narrowing (KB, JM), pp. 113–129.
CAVCAV-2014-CavadaCDGMMMRT
The nuXmv Symbolic Model Checker (RC, AC, MD, AG, AM, AM, SM, MR, ST), pp. 334–342.
CAVCAV-2014-CermakLMM #logic #named #specification #verification
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PC, AL, FM, AM), pp. 525–532.
CAVCAV-2014-InversoT0TP #bound #c #concurrent #lazy evaluation #multi #source code #thread
Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization (OI, ET, BF, SLT, GP), pp. 585–602.
CAVCAV-2014-KomuravelliGC #recursion #smt #source code
SMT-Based Model Checking for Recursive Programs (AK, AG, SC), pp. 17–34.
LICSLICS-CSL-2014-BaierDK #analysis #probability #trade-off
Trade-off analysis meets probabilistic model checking (CB, CD, SK), p. 10.
LICSLICS-CSL-2014-BojanczykDK #calculus #composition #theorem #μ-calculus
Decomposition theorems and model-checking for the modal μ-calculus (MB, CD, SK), p. 10.
LICSLICS-CSL-2014-BovaGS #logic #order #set
Model checking existential logic on partially ordered sets (SB, RG, SS), p. 10.
LICSLICS-CSL-2014-TsukadaO #composition #game studies #higher-order
Compositional higher-order model checking via ω-regular games over Böhm trees (TT, CHLO), p. 10.
TAPTAP-2014-ArcainiGR #abstraction #testing
An Abstraction Technique for Testing Decomposable Systems by Model Checking (PA, AG, ER), pp. 36–52.
VMCAIVMCAI-2014-AminofJKR
Parameterized Model Checking of Token-Passing Systems (BA, SJ, AK, SR), pp. 262–281.
CIAACIAA-2013-DeganoFM #towards
Towards Nominal Context-Free Model-Checking (PD, GLF, GM), pp. 109–121.
ICALPICALP-v1-2013-Lampis #bound #graph
Model Checking Lower Bounds for Simple Graphs (ML), pp. 673–683.
ICALPICALP-v2-2013-GanianHKOST #graph
FO Model Checking of Interval Graphs (RG, PH, DK, JO, JS, JT), pp. 250–262.
LATALATA-2013-Ong #automaton #higher-order #recursion
Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking (LO), pp. 13–41.
LATALATA-2013-Quaas #automaton #logic #metric
Model Checking Metric Temporal Logic over Automata with One Counter (KQ), pp. 468–479.
IFMIFM-2013-Larsen #automaton #statistics
Priced Timed Automata and Statistical Model Checking (KGL), pp. 154–161.
IFMIFM-2013-SongT #api #library
Model-Checking Software Library API Usage Rules (FS, TT), pp. 192–207.
RTARTA-2013-BaeEM #infinity #logic #using
Abstract Logical Model Checking of Infinite-State Systems Using Narrowing (KB, SE, JM), pp. 81–96.
SEFMSEFM-2013-BorekMSR #approach #modelling
Model Checking of Security-Critical Applications in a Model-Driven Approach (MB, NM, KS, WR), pp. 76–90.
SFMSFM-2013-BrimCS #biology
Model Checking of Biological Systems (LB, MC, DS), pp. 63–112.
HCIHCI-AMTE-2013-BratMP #interactive #semantics
V&V of Lexical, Syntactic and Semantic Properties for Interactive Systems through Model Checking of Formal Description of Dialog (GB, CM, PAP), pp. 290–299.
MODELSMoDELS-2013-ZurowskaD #composition #lazy evaluation #modelling #uml #using
Model Checking of UML-RT Models Using Lazy Composition (KZ, JD), pp. 304–319.
HILTHILT-2013-Chaki #bound
Bounded model checking of high-integrity software (SC), pp. 9–10.
LOPSTRLOPSTR-2013-Seki #logic programming #source code
Extending Co-logic Programs for Branching-Time Model Checking (HS), pp. 127–144.
PEPMPEPM-2013-SatoUK #higher-order #scalability #source code #towards
Towards a scalable software model checker for higher-order programs (RS, HU, NK), pp. 53–62.
ASEASE-2013-ArthoHPTWY #communication #distributed
Software model checking for distributed systems with selector-based, non-blocking communication (CA, MH, RP, YT, FW, MY), pp. 169–179.
ASEASE-2013-ChoDS #bound #composition #named #source code
BLITZ: Compositional bounded model checking for real-world programs (CYC, VD, DS), pp. 136–146.
ASEASE-2013-FalkeMS #bound
The bounded model checker LLBMC (SF, FM, CS), pp. 706–709.
ESEC-FSEESEC-FSE-2013-LiuL0ZWD #named #self #state machine #uml
USMMC: a self-contained model checker for UML state machines (SL, YL, JS, MZ, BW, JSD), pp. 623–626.
ESEC-FSEESEC-FSE-2013-SongT #automaton #detection #named
PoMMaDe: pushdown model-checking for malware detection (FS, TT), pp. 607–610.
ESEC-FSEESEC-FSE-2013-ZervoudakisREF #verification
Cascading verification: an integrated method for domain-specific model checking (FZ, DSR, SGE, AF), pp. 400–410.
ICSEICSE-2013-CordySHL #multi #product line
Beyond boolean product-line model checking: dealing with feature attributes and multi-features (MC, PYS, PH, AL), pp. 472–481.
ICSEICSE-2013-DongSL
Build your own model checker in one month (JSD, JS, YL), pp. 1481–1483.
ICSEICSE-2013-TianD #detection
Detecting spurious counterexamples efficiently in abstract model checking (CT, ZD), pp. 202–211.
DACDAC-2013-WuWLH #algorithm #generative #satisfiability
A counterexample-guided interpolant generation algorithm for SAT-based model checking (CYW, CAW, CYL, CY(H), p. 6.
DATEDATE-2013-CabodiLV #bound #optimisation
Optimization techniques for craig interpolant compaction in unbounded model checking (GC, CL, DV), pp. 1417–1422.
DATEDATE-2013-FakihGFR #analysis #architecture #performance #towards #using
Towards performance analysis of SDFGs mapped to shared-bus architectures using model-checking (MF, KG, MF, AR), pp. 1167–1172.
DATEDATE-2013-WelpK #reachability
QF BV model checking with property directed reachability (TW, AK), pp. 791–796.
ESOPESOP-2013-KobayashiI #higher-order #recursion #source code
Model-Checking Higher-Order Programs with Recursive Types (NK, AI), pp. 431–450.
FASEFASE-2013-BeyerL
Explicit-State Software Model Checking Based on CEGAR and Interpolation (DB, SL), pp. 146–162.
TACASTACAS-2013-BenediktLW #ltl #markov
LTL Model Checking of Interval Markov Chains (MB, RL, JW), pp. 32–46.
TACASTACAS-2013-ChenFKPS #game studies #multi #named #probability
PRISM-games: A Model Checker for Stochastic Multi-Player Games (TC, VF, MZK, DP, AS), pp. 185–191.
TACASTACAS-2013-FalkeMS #bound #c #contest #named #source code #using
LLBMC: Improved Bounded Model Checking of C Programs Using LLVM — (Competition Contribution) (SF, FM, CS), pp. 623–626.
TACASTACAS-2013-GangeNSSS #bound #constraints #regular expression
Unbounded Model-Checking with Interpolation for Regular Language Constraints (GG, JAN, PJS, HS, PS), pp. 277–291.
TACASTACAS-2013-GligoricM #database
Model Checking Database Applications (MG, RM), pp. 549–564.
TACASTACAS-2013-HuangSW #game studies
Model-Checking Iterated Games (CHH, SS, FW), pp. 154–168.
TACASTACAS-2013-KoleiniRR #data access #policy
Model Checking Agent Knowledge in Dynamic Access Control Policies (MK, ER, MR), pp. 448–462.
TACASTACAS-2013-MateescuS #model transformation #named #π-calculus
PIC2LNT: Model Transformation for Model Checking an Applied π-Calculus (RM, GS), pp. 192–198.
TACASTACAS-2013-RenaultDKP #automaton #composition #performance
Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking (ER, ADL, FK, DP), pp. 580–593.
TACASTACAS-2013-SongT #detection #ltl
LTL Model-Checking for Malware Detection (FS, TT), pp. 416–431.
CAVCAV-2013-AlglaveKT #bound #concurrent #partial order #performance
Partial Orders for Efficient Bounded Model Checking of Concurrent Software (JA, DK, MT), pp. 141–157.
CAVCAV-2013-BarnatBHHKLRSW #c #c++ #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-BinghamBEG #concurrent #distributed
Distributed Explicit State Model Checking of Deadlock Freedom (BDB, JDB, JE, MRG), pp. 235–241.
CAVCAV-2013-BrimCDS #parametricity #probability #using
Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking (LB, MC, SD, DS), pp. 107–123.
CAVCAV-2013-ChatterjeeGK #automaton #ltl #probability #synthesis
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis (KC, AG, JK), pp. 559–575.
CAVCAV-2013-ClaessenFIPW #network #reachability #set
Model-Checking Signal Transduction Networks through Decreasing Reachability Sets (KC, JF, SI, NP, QW), pp. 85–100.
CAVCAV-2013-ColangeBKT #diagrams #distributed #towards #using
Towards Distributed Software Model-Checking Using Decision Diagrams (MC, SB, FK, YTM), pp. 830–845.
CAVCAV-2013-EsparzaLNNSS #execution #ltl
A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.
CAVCAV-2013-HeizmannHP #automaton #people
Software Model Checking for People Who Love Automata (MH, JH, AP), pp. 36–52.
CAVCAV-2013-JegourelLS #statistics
Importance Splitting for Statistical Model Checking Rare Properties (CJ, AL, SS), pp. 576–591.
CAVCAV-2013-KomuravelliGCC #abstraction #automation #bound #smt
Automatic Abstraction in SMT-Based Unbounded Software Model Checking (AK, AG, SC, EMC), pp. 846–862.
CAVCAV-2013-ManciniMMMMT #simulation #verification
System Level Formal Verification via Model Checking Driven Simulation (TM, FM, AM, IM, FM, ET), pp. 296–312.
CAVCAV-2013-PrabhakarS #abstraction #hybrid
Abstraction Based Model-Checking of Stability of Hybrid Systems (PP, MGS), pp. 280–295.
CAVCAV-2013-StewartEY #automaton #bound #polynomial #probability
Upper Bounds for Newton’s Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata (AS, KE, MY), pp. 495–510.
CSLCSL-2013-BroadbentK #higher-order #recursion
Saturation-Based Model Checking of Higher-Order Recursion Schemes (CHB, NK), pp. 129–148.
CSLCSL-2013-Goller #concurrent #parametricity
The Fixed-Parameter Tractability of Model Checking Concurrent Systems (SG), pp. 332–347.
ICSTICST-2013-Torsel #domain-specific language #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.
ICSTICST-2013-YeolekarUAKV #generative #scalability #testing #using
Scaling Model Checking for Test Generation Using Dynamic Inference (AY, DU, VA, SK, RV), pp. 184–191.
ISSTAISSTA-2013-GuiSLSDW #predict #reliability #testing
Combining model checking and testing with an application to reliability prediction and distribution (LG, JS, YL, YJS, JSD, XW), pp. 101–111.
LICSLICS-2013-BolligKM #complexity #multi
The Complexity of Model Checking Multi-stack Systems (BB, DK, RM), pp. 163–172.
LICSLICS-2013-BoralS #parse tree
Model-Checking Parse Trees (AB, SS), pp. 153–162.
LICSLICS-2013-EickmeyerKK #first-order #graph #invariant #logic
Model Checking for Successor-Invariant First-Order Logic on Minor-Closed Graph Classes (KE, KiK, SK), pp. 134–142.
CBSECBSE-2012-BenesBCO #analysis #component #development #probability #reliability
Reliability analysis in component-based development via probabilistic model checking (NB, BB, IC, RO), pp. 83–92.
LATALATA-2012-TangO #automaton #on the
On Model Checking for Visibly Pushdown Automata (NVT, HO), pp. 408–419.
FMFM-2012-GrumbergMY #behaviour #modelling #uml
Applying Software Model Checking Techniques for Behavioral UML Models (OG, YM, KY), pp. 277–292.
FMFM-2012-SongT #detection #performance #using
Efficient Malware Detection Using Model-Checking (FS, TT), pp. 418–433.
IFMIFM-2012-RochaBCN #bound #comprehension #debugging #programming #using
Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples (HR, RSB, LCC, ADN), pp. 128–142.
IFMIFM-2012-ZhangNN #revisited #static analysis
Model Checking as Static Analysis: Revisited (FZ, FN, HRN), pp. 99–112.
SEFMSEFM-2012-AbdelhalimST #approach #effectiveness #optimisation
An Optimization Approach for Effective Formalized fUML Model Checking (IA, SS, HT), pp. 248–262.
FLOPSFLOPS-2012-TobitaTK #analysis #higher-order
Exact Flow Analysis by Higher-Order Model Checking (YT, TT, NK), pp. 275–289.
ICFPICFP-2012-NeatherwayRO #algorithm #higher-order
A traversal-based algorithm for higher-order model checking (RPN, SJR, CHLO), pp. 353–364.
GT-VMTGT-VMT-2012-Heussner #communication #graph #graph grammar #process
Model Checking Communicating Processes: Run Graphs, Graph Grammars, and MSO (AH).
ICEISICEIS-v2-2012-AokiOOM #quality #requirements #specification #using
Quality Improvement of Requirements Specification using Model Checking Technique (YA, SO, HO, SM), pp. 401–406.
ICEISICEIS-v2-2012-CapelM #approach #automation #composition #correctness #safety #verification
A Formal Compositional Verification Approach for Safety-Critical Systems Correctness — Model-Checking based Methodological Approach to Automatically Verify Safety Critical Systems Software (MIC, LEMM), pp. 105–112.
KRKR-2012-GiordanoMD #bound
Achieving Completeness in Bounded Model Checking of Action Theories in ASP (LG, AM, DTD).
AdaEuropeAdaEurope-2012-FariaMP #ada #approach #source code
An Approach to Model Checking Ada Programs (JMF, JM, JSP), pp. 105–118.
LOPSTRLOPSTR-2012-AngelisFPP
Specialization with Constrained Generalization for Software Model Checking (EDA, FF, AP, MP), pp. 51–70.
QAPLQAPL-2012-BulychevDLMPLW #automaton #named #statistics
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata (PEB, AD, KGL, MM, DBP, AL, ZW), pp. 1–16.
QAPLQAPL-2012-CormieBowinsB #ltl #probability
Measuring Progress of Probabilistic LTL Model Checking (ECB, FvB), pp. 33–47.
QAPLQAPL-2012-Giro #performance
Efficient computation of exact solutions for quantitative model checking (SG), pp. 17–32.
ASEASE-2012-SongT #named #source code
PuMoC: a CTL model-checker for sequential programs (FS, TT), pp. 346–349.
FSEFSE-2012-BeyerHKW #verification
Conditional model checking: a technique to pass information between verifiers (DB, TAH, MEK, PW), p. 57.
ICSEICSE-2012-CordyCPSHL #abstraction #product line
Simulation-based abstractions for software product-line model checking (MC, AC, GP, PYS, PH, AL), pp. 672–682.
ICSEICSE-2012-SongHLSLD #approach #multi #probability
Analyzing multi-agent systems with probabilistic model checking approach (SS, JH, YL, JS, HfL, JSD), pp. 1337–1340.
SACSAC-2012-KeshishzadehIM #automaton #framework
A Büchi automata based model checking framework for reo connectors (SK, MI, AM), pp. 1536–1543.
SACSAC-2012-PerroneDH #graph
A model checker for Bigraphs (GP, SD, TTH), pp. 1320–1325.
DACDAC-2012-ChouHHH #design
Symbolic model checking on SystemC designs (CNC, YSH, CH, CY(H), pp. 327–333.
DATEDATE-2012-TheelenKW #data flow
Model checking of Scenario-Aware Dataflow with CADP (BDT, JPK, HW), pp. 653–658.
FoSSaCSFoSSaCS-2012-BolligCGK #word
Model Checking Languages of Data Words (BB, AC, PG, KNK), pp. 391–405.
FoSSaCSFoSSaCS-2012-GollerHOW #automaton #parametricity
Branching-Time Model Checking of Parametric One-Counter Automata (SG, CH, JO, JW), pp. 406–420.
FoSSaCSFoSSaCS-2012-Kartzow #automaton #exponential #first-order
First-Order Model Checking on Nested Pushdown Trees is Complete for Doubly Exponential Alternating Time (AK), pp. 376–390.
TACASTACAS-2012-BarbotHP #statistics
Coupling and Importance Sampling for Statistical Model Checking (BB, SH, CP), pp. 331–346.
TACASTACAS-2012-CairesV #concurrent #logic #named #specification
SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications (LC, HTV), pp. 485–491.
TACASTACAS-2012-CordeiroMNF #bound #contest
Context-Bounded Model Checking with ESBMC 1.17 — (Competition Contribution) (LCC, JM, DN, BF), pp. 534–537.
TACASTACAS-2012-HolzlN #verification
Verifying pCTL Model Checking (JH, TN), pp. 347–361.
TACASTACAS-2012-JegourelLS #framework #performance #platform #statistics
A Platform for High Performance Statistical Model Checking — PLASMA (CJ, AL, SS), pp. 498–503.
TACASTACAS-2012-JinYS #java #memory management
Java Memory Model-Aware Model Checking (HJ, TYK, BAS), pp. 220–236.
TACASTACAS-2012-LangM #equation #lts #network #using
Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems (FL, RM), pp. 141–156.
TACASTACAS-2012-SinzMF #bound #contest #named #representation
LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation — (Competition Contribution) (CS, FM, SF), pp. 542–544.
TACASTACAS-2012-SongT #automaton #detection
Pushdown Model Checking for Malware Detection (FS, TT), pp. 110–125.
WRLAWRLA-2012-BaeM #locality
Model Checking LTLR Formulas under Localized Fairness (KB, JM), pp. 99–117.
WRLAWRLA-2012-LepriAO #maude #realtime
Timed CTL Model Checking in Real-Time Maude (DL, , PCÖ), pp. 182–200.
CAVCAV-2012-CimattiG
Software Model Checking via IC3 (AC, AG), pp. 277–293.
CAVCAV-2012-ConchonGKMZ #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-Dill #biology
Model Checking Cell Biology (DLD), p. 2.
CAVCAV-2012-HassanBS #incremental #induction
Incremental, Inductive CTL Model Checking (ZH, ARB, FS), pp. 532–547.
CAVCAV-2012-JegourelLS #optimisation #parametricity #statistics
Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking (CJ, AL, SS), pp. 327–342.
CAVCAV-2012-RolliniSS
Leveraging Interpolant Strength in Model Checking (SFR, OS, NS), pp. 193–209.
CAVCAV-2012-SongSLD #probability #realtime
A Model Checker for Hierarchical Probabilistic Real-Time Systems (SS, JS, YL, JSD), pp. 705–711.
ICLPICLP-2012-Angelis
Software Model Checking by Program Specialization (EDA), pp. 439–444.
ICLPICLP-J-2012-GorlinRS #logic programming #probability
Model checking with probabilistic tabled logic programming (AG, CRR, SAS), pp. 681–700.
ICSTICST-2012-GligoricMM #named #programming language
X10X: Model Checking a New Programming Language with an “Old” Model Checker (MG, PCM, DM), pp. 11–20.
IJCARIJCAR-2012-EmmerKKSV #bound #word
EPR-Based Bounded Model Checking at Word Level (ME, ZK, KK, CS, AV), pp. 210–224.
LICSLICS-2012-BundalaOW #bound #on the
On the Magnitude of Completeness Thresholds in Bounded Model Checking (DB, JO, JW), pp. 155–164.
LICSLICS-2012-EngelmannKS #first-order #higher-order #monad
First-Order and Monadic Second-Order Model-Checking on Ordered Structures (VE, SK, SS), pp. 275–284.
TAPTAP-2012-ArmandoPCMB #automation #protocol #security #testing
From Model-Checking to Automated Testing of Security Protocols: Bridging the Gap (AA, GP, RC, AM, DB), pp. 3–18.
TAPTAP-2012-Pasareanu #execution #symbolic computation #testing
Combining Model Checking and Symbolic Execution for Software Testing (CSP), p. 2.
VMCAIVMCAI-2012-Bugaychenko #diagrams #multi #on the #probability
On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking (DB), pp. 104–118.
VMCAIVMCAI-2012-DimitrovaFKRS #data flow
Model Checking Information Flow in Reactive Systems (RD, BF, MK, MNR, HS), pp. 169–185.
ICALPICALP-v2-2011-FischerK #calculus #hybrid #linear #μ-calculus
Model Checking the Quantitative μ-Calculus on Linear Hybrid Systems (DF, LK), pp. 404–415.
ICALPICALP-v2-2011-ZhangB #probability
A Progress Measure for Explicit-State Probabilistic Model-Checkers (XZ, FvB), pp. 283–294.
ICALPICALP-v2-2011-ZhangJNH
Automata-Based CSL Model Checking (LZ, DNJ, FN, HH), pp. 271–282.
SEFMSEFM-2011-MorseCNF #bound #ltl
Context-Bounded Model Checking of LTL Properties for ANSI-C Software (JM, LCC, DN, BF), pp. 302–317.
SEFMSEFM-2011-VassevH #case study #experience
Developing Model-Checking Mechanisms for ASSL: An Experience Report (EV, MH), pp. 19–34.
GT-VMTGT-VMT-2011-VandinL #graph #maude #towards
Towards a Maude Tool for Model Checking Temporal Graph Properties (AV, ALL).
SEKESEKE-2011-ChenF #aspectj
Model Checking Framework-based Applications with AspectJ Assistance (ZC, SF), pp. 296–301.
MODELSMoDELS-2011-MoffettBD #consistency #protocol #uml #using #verification
Verifying UML-RT Protocol Conformance Using Model Checking (YM, AB, JD), pp. 410–424.
SPLCSPLC-2011-GhezziS #approach #non-functional #parametricity #performance #product line #towards #using #verification
Verifying Non-functional Properties of Software Product Lines: Towards an Efficient Approach Using Parametric Model Checking (CG, AMS), pp. 170–174.
PLDIPLDI-2011-KobayashiSU #abstraction #higher-order
Predicate abstraction and CEGAR for higher-order model checking (NK, RS, HU), pp. 222–233.
SASSAS-2011-MonniauxG #bound #fixpoint #using
Using Bounded Model Checking to Focus Fixpoint Iterations (DM, LG), pp. 369–385.
ASEASE-2011-LeungwattanakitAHTY #distributed #process
Model checking distributed systems by combining caching and process checkpointing (WL, CA, MH, YT, MY), pp. 103–112.
ASEASE-2011-MehlitzTU #named #user interface
JPF-AWT: Model checking GUI applications (PCM, OT, MU), pp. 584–587.
ASEASE-2011-NguyenSLD #framework
A model checking framework for hierarchical systems (TKN, JS, YL, JSD), pp. 633–636.
ASEASE-2011-VakiliD #declarative #modelling #using
Using model checking to analyze static properties of declarative models (AV, NAD), pp. 428–431.
ICSEICSE-2011-ClassenHSL #product line
Symbolic model checking of software product lines (AC, PH, PYS, AL), pp. 321–330.
ICSEICSE-2011-CordeiroF #bound #concurrent #multi #smt #thread #using #verification
Verifying multi-threaded software using smt-based context-bounded model checking (LC, BF), pp. 331–340.
ICSEICSE-2011-FilieriGT #performance #probability #runtime
Run-time efficient probabilistic model checking (AF, CG, GT), pp. 341–350.
DATEDATE-2011-CabodiN #multi
Optimized model checking of multiple properties (GC, SN), pp. 543–546.
SOSPSOSP-2011-GuoWZHYZ #interface #reduction
Practical software model checking via dynamic interface reduction (HG, MW, LZ, GH, JY, LZ), pp. 265–278.
FASEFASE-2011-LiXBL #automaton
Model Checking Büchi Pushdown Systems (JL, FX, TB, VL), pp. 141–155.
FASEFASE-2011-OudinetDGLP #monte carlo
Uniform Monte-Carlo Model Checking (JO, AD, MCG, RL, SP), pp. 127–140.
FoSSaCSFoSSaCS-2011-Kobayashi #algorithm #automaton #higher-order #linear #recursion
A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes (NK0), pp. 260–274.
TACASTACAS-2011-BarbotCHKM #linear #performance #realtime
Efficient CTMC Model Checking of Linear Real-Time Objectives (BB, TC, TH, JPK, AM), pp. 128–142.
TACASTACAS-2011-TalupurH #using
Biased Model Checking Using Flows (MT, HH), pp. 239–253.
CAVCAV-2011-BaeM #ltl #parametricity
State/Event-Based LTL Model Checking under Parametric Generalized Fairness (KB, JM), pp. 132–148.
CAVCAV-2011-BuchholzHHZ #algorithm
Model Checking Algorithms for CTMDPs (PB, EMH, HH, LZ), pp. 225–242.
CAVCAV-2011-CimattiGMNR #named
Kratos — A Software Model Checker for SystemC (AC, AG, AM, IN, MR), pp. 310–316.
CAVCAV-2011-DavidLLMW #realtime #statistics
Time for Statistical Model Checking of Real-Time Systems (AD, KGL, AL, MM, ZW), pp. 349–355.
CAVCAV-2011-HagueL #data type #recursion #source code
Model Checking Recursive Programs with Numeric Data Types (MH, AWL), pp. 743–759.
CAVCAV-2011-KroeningOSWW #bound #linear
Linear Completeness Thresholds for Bounded Model Checking (DK, JO, OS, TW, JW), pp. 557–572.
CAVCAV-2011-MorbePS #automaton
Fully Symbolic Model Checking for Timed Automata (GM, FP, CS), pp. 616–632.
ICSTICST-2011-KeatingMH #implementation
Model Checking a TTCAN Implementation (DK, AM, MPH), pp. 387–396.
LICSLICS-2011-Kobayashi #higher-order #theory and practice
Higher-Order Model Checking: From Theory to Practice (NK0), pp. 219–224.
VMCAIVMCAI-2011-Bradley #satisfiability
SAT-Based Model Checking without Unrolling (ARB), pp. 70–87.
VMCAIVMCAI-2011-LopesR #distributed #predict
Distributed and Predictable Software Model Checking (NPL, AR), pp. 340–355.
CSMRCSMR-2010-LuciaDGR #behaviour #design pattern #detection
Improving Behavioral Design Pattern Detection through Model Checking (ADL, VD, CG, MR), pp. 176–185.
ICSMEICSM-2010-Letarte #interprocedural #performance #static analysis
Conversion of fast inter-procedural static analysis to model checking (DL), pp. 1–2.
ICALPICALP-v2-2010-GollerHOW #automaton #parametricity
Model Checking Succinct and Parametric One-Counter Automata (SG, CH, JO, JW), pp. 575–586.
IFMIFM-2010-Baier #distributed #on the #random
On Model Checking Techniques for Randomized Distributed Systems (CB), pp. 1–11.
IFMIFM-2010-BouchenebIN #algorithm #replication
Symbolic Model-Checking of Optimistic Replication Algorithms (HB, AI, MN), pp. 89–104.
SEFMSEFM-2010-BenettiMV #ad hoc #network #protocol
Model Checking Ad Hoc Network Routing Protocols: ARAN vs. endairA (DB, MM, LV), pp. 191–202.
SEFMSEFM-2010-LindsayWY #assessment #behaviour #safety #using
Safety Assessment Using Behavior Trees and Model Checking (PAL, KW, NY), pp. 181–190.
SEKESEKE-2010-ZhangZH #precise
Some Improvements for More Precise Model Checking (ZZ, QZ, MH), pp. 106–112.
OOPSLAOOPSLA-2010-RobersonB #composition #performance
Efficient modular glass box software model checking (MR, CB), pp. 4–21.
ASEASE-2010-HalleEBB #fault #navigation #runtime #state machine #web
Eliminating navigation errors in web applications via model checking and runtime enforcement of navigation state machines (SH, TE, CB, TB), pp. 235–244.
ASEASE-2010-HeJBGW #approach #bound #statistics
A bounded statistical approach for model checking of unbounded until properties (RH, PJ, SB, APG, HW), pp. 225–234.
ASEASE-2010-KimYS #debugging #memory management #named #using
JRF-E: using model checking to give advice on eliminating memory model-related bugs (KK, TYK, BAS), pp. 215–224.
ASEASE-2010-Letarte #analysis #graph #interprocedural #precise #representation
Model checking graph representation of precise boolean inter-procedural flow analysis (DL), pp. 511–516.
ICSEICSE-2010-ClassenHSLR #performance #product line #verification
Model checking lots of systems: efficient verification of temporal properties in software product lines (AC, PH, PYS, AL, JFR), pp. 335–344.
ICSEICSE-2010-Cordeiro #bound #concurrent #embedded #multi #smt #thread
SMT-based bounded model checking for multi-threaded software in embedded systems (LC), pp. 373–376.
SACSAC-2010-Fellah #automaton #framework
Time and alternation: an automata based framework to software model checking (AF), pp. 2498–2502.
DACDAC-2010-ChocklerKP
Coverage in interpolation-based model checking (HC, DK, MP), pp. 182–187.
FoSSaCSFoSSaCS-2010-DemriS #decidability #ltl
When Model-Checking Freeze LTL over Counter Machines Becomes Decidable (SD, AS), pp. 176–190.
FoSSaCSFoSSaCS-2010-NielsonN #logic #static analysis
Model Checking Is Static Analysis of Modal Logic (FN, HRN), pp. 191–205.
FoSSaCSFoSSaCS-2010-ToL #algorithm #decidability #infinity #ltl
Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems (AWT, LL), pp. 221–236.
TACASTACAS-2010-BaslerHKOWZ #named
Boom: Taking Boolean Program Model Checking One Step Further (GB, MH, DK, CHLO, TW, HZ), pp. 145–149.
TACASTACAS-2010-DragerKFW #concurrent #infinity #named
SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems (KD, AK, BF, HW), pp. 271–274.
TACASTACAS-2010-MalinowskiN #automaton #bound #partial order #satisfiability #semantics
SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata (JM, PN), pp. 405–419.
TACASTACAS-2010-ZhangN #interactive #markov
Model Checking Interactive Markov Chains (LZ, MRN), pp. 53–68.
WRLAWRLA-2010-BaeM #linear #logic #maude
The Linear Temporal Logic of Rewriting Maude Model Checker (KB, JM), pp. 208–225.
CAVCAV-2010-BozzanoCKNNRW
A Model Checker for AADL (MB, AC, JPK, VYN, TN, MR, RW), pp. 562–565.
CAVCAV-2010-Caniart #named
Merit: An Interpolating Model-Checker (NC), pp. 162–166.
CAVCAV-2010-CernyRZCA #concurrent #implementation
Model Checking of Linearizability of Concurrent List Implementations (PC, AR, DZ, SC, RA), pp. 465–479.
CAVCAV-2010-FerranteMNPS
A NuSMV Extension for Graded-CTL Model Checking (AF, MM, MN, MP, FS), pp. 670–673.
CAVCAV-2010-GrafPQ #distributed
Achieving Distributed Control through Model Checking (SG, DP, SQ), pp. 396–409.
CAVCAV-2010-HahnHWZ #markov #modelling #named #parametricity
PARAM: A Model Checker for Parametric Markov Models (EMH, HH, BW, LZ), pp. 660–664.
CAVCAV-2010-TorreMP #concurrent #interface #linear #source code #using
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces (SLT, PM, GP), pp. 629–644.
ICSTICST-2010-LodingP #automaton #generative #testing
Timed Moore Automata: Test Data Generation and Model Checking (HL, JP), pp. 449–458.
ICSTICST-2010-PavlovicE #diagrams
Model Checking PLC Software Written in Function Block Diagram (OP, HDE), pp. 439–448.
IJCARIJCAR-2010-GhilardiR #modulo theories #named
MCMT: A Model Checker Modulo Theories (SG, SR), pp. 22–29.
ICSTSAT-2010-MillerKLB #bound #design #encoding
Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs (CM, SK, MDTL, BB), pp. 194–208.
VMCAIVMCAI-2010-AminofKM
Improved Model Checking of Hierarchical Systems (BA, OK, AM), pp. 61–77.
VMCAIVMCAI-2010-Katoen #probability #roadmap
Advances in Probabilistic Model Checking (JPK), p. 25.
VMCAIVMCAI-2010-SridharH #monitoring
Model-Checking In-Lined Reference Monitors (MS, KWH), pp. 312–327.
CBSECBSE-2009-LiCHMC #component #fault tolerance
Selecting Fault Tolerant Styles for Third-Party Components with Model Checking Support (JL, XC, GH, HM, FC), pp. 69–86.
ICSMEICSM-2009-YangDR
Regression model checking (GY, MBD, GR), pp. 115–124.
SCAMSCAM-2009-AchenbachO #abstraction #testing
Engineering Abstractions in Model Checking and Testing (MA, KO), pp. 137–146.
CIAACIAA-2009-CourbisHK #approximate
TAGED Approximations for Temporal Properties Model-Checking (RC, PCH, OK), pp. 135–144.
ICALPICALP-v2-2009-KobayashiO #calculus #complexity #recursion #μ-calculus
Complexity of Model Checking Recursion Schemes for Fragments of the Modal μ-Calculus (NK, CHLO), pp. 223–234.
FMFM-2009-LiuCLS #refinement
Model Checking Linearizability via Refinement (YL, WC, YAL, JS), pp. 321–337.
FMFM-2009-PradellaMP #bound #encoding #metric
A Metric Encoding for Bounded Model Checking (MP, AM, PSP), pp. 741–756.
FMFM-2009-SunLRLD #abstraction #process
Fair Model Checking with Process Counter Abstraction (JS, YL, AR, SL, JSD), pp. 123–139.
FMFM-2009-Tonetta #abstraction
Abstract Model Checking without Computing the Abstraction (ST), pp. 89–105.
IFMIFM-2009-VargasGTG #ltl
Model Checking LTL Formulae in RAISE with FDR (APV, AGG, SLTT, CG), pp. 231–245.
IFMIFM-2009-YangASHSG #reduction
Dynamic Path Reduction for Software Model Checking (ZY, BAR, KAS, XH, SAS, RG), pp. 322–336.
SEFMSEFM-2009-BertoliniM #probability #testing #user interface #using
Using Probabilistic Model Checking to Evaluate GUI Testing Techniques (CB, AM), pp. 115–124.
SEFMSEFM-2009-BuiN #heuristic
Heuristic Sensitivity in Guided Random-Walk Based Model Checking (THB, AN), pp. 125–134.
SEFMSEFM-2009-NgocO #analysis #fault
Overflow and Roundoff Error Analysis via Model Checking (DTBN, MO), pp. 105–114.
AdaEuropeAdaEurope-2009-BuchsLC #generative #modelling #process #testing
Model Checking Techniques for Test Generation from Business Process Models (DB, LL, AC), pp. 59–74.
PEPMPEPM-2009-RungtaM #morphism #polymorphism #source code
Guided model checking for programs with polymorphism (NR, EGM), pp. 21–30.
POPLPOPL-2009-BrunelDHLM #logic #using
A foundation for flow-based program matching: using temporal logic and model checking (JB, DD, RRH, JLL, GM), pp. 114–126.
PPDPPPDP-2009-Kobayashi #higher-order
Model-checking higher-order functions (NK), pp. 25–36.
SASSAS-2009-WehrleH #graph
The Causal Graph Revisited for Directed Model Checking (MW, MH), pp. 86–101.
ASEASE-2009-ArthoLHTY #branch #linear
Cache-Based Model Checking of Networked Applications: From Linear to Branching Time (CA, WL, MH, YT, MY), pp. 447–458.
ASEASE-2009-BarnatBS #clustering #ltl
Cluster-Based I/O-Efficient LTL Model Checking (JB, LB, PS), pp. 635–639.
ASEASE-2009-CordeiroFM #bound #embedded #smt
SMT-Based Bounded Model Checking for Embedded ANSI-C Software (LCC, BF, JMS), pp. 137–148.
ASEASE-2009-KimYS #concurrent #detection #heuristic #memory management #precise #using
Precise Data Race Detection in a Relaxed Memory Model Using Heuristic-Based Model Checking (KK, TYK, BAS), pp. 495–499.
ASEASE-2009-LauenrothPT #product line
Model Checking of Domain Artifacts in Product Line Engineering (KL, KP, ST), pp. 269–280.
SACSAC-2009-CasadeiV #design #probability #self #simulation #using
Using probabilistic model checking and simulation for designing self-organizing systems (MC, MV), pp. 2103–2104.
CASECASE-2009-VoronovA #process #using #verification
Verification of process operations using model checking (AV, ), pp. 415–420.
DATEDATE-2009-CabodiCGMNQ #constraints #verification
Speeding up model checking by exploiting explicit and hidden verification constraints (GC, PC, LG, MM, SN, SQ), pp. 1686–1691.
FoSSaCSFoSSaCS-2009-BroadbentO #higher-order #on the #recursion
On Global Model Checking Trees Generated by Higher-Order Recursion Schemes (CHB, CHLO), pp. 107–121.
TACASTACAS-2009-LimeRST #named #parametricity #petri net
Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches (DL, OHR, CS, LMT), pp. 54–57.
TACASTACAS-2009-Miller #development #modelling
Bridging the Gap Between Model-Based Development and Model Checking (SPM), pp. 443–453.
TACASTACAS-2009-NguyenR #garbage collection
Memoised Garbage Collection for Software Model Checking (VYN, TCR), pp. 201–214.
TACASTACAS-2009-WehrleKP
Transition-Based Directed Model Checking (MW, SK, AP), pp. 186–200.
CAVCAV-2009-BasuBPS #distributed #scheduling
Priority Scheduling of Distributed Systems Based on Model Checking (AB, SB, DP, JS), pp. 79–93.
CAVCAV-2009-HahnHWZ #infinity #markov #named
INFAMY: An Infinite-State Markov Model Checker (EMH, HH, BW, LZ), pp. 641–647.
CAVCAV-2009-HopkinsO #equivalence #higher-order #named
Homer: A Higher-Order Observational Equivalence Model checkER (DH, CHLO), pp. 654–660.
CAVCAV-2009-LomuscioQR #multi #named #verification
MCMAS: A Model Checker for the Verification of Multi-Agent Systems (AL, HQ, FR), pp. 682–688.
CSLCSL-2009-GuoWXC #on the
On Model Checking Boolean BI (HG, HW, ZX, YC), pp. 302–316.
CSLCSL-2009-To #process
Model Checking FO(R) over One-Counter Processes and beyond (AWT), pp. 485–499.
ICSTICST-2009-FraserG #evaluation #generative #specification #testing
An Evaluation of Model Checkers for Specification Based Test Case Generation (GF, AG), pp. 41–50.
ICSTICST-2009-PostS #bound #equivalence #functional #implementation #proving #using
Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking (HP, CS), pp. 31–40.
LICSLICS-2009-ChenHKM #automaton #markov #specification
Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications (TC, TH, JPK, AM), pp. 309–318.
LICSLICS-2009-KobayashiO #calculus #higher-order #recursion #type system #μ-calculus
A Type System Equivalent to the Modal μ-Calculus Model Checking of Higher-Order Recursion Schemes (NK, CHLO), pp. 179–188.
TAPTAP-2009-HerberFG #process #testing
Combining Model Checking and Testing in a Continuous HW/SW Co-verification Process (PH, FF, SG), pp. 121–136.
TAPTAP-2009-Rapin #bound #execution #symbolic computation
Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables (NR), pp. 137–152.
FATESTestCom-FATES-2009-WieczorekKRLBPS #integration #modelling #testing
Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models (SW, VK, AR, ML, JB, DP, IS), pp. 179–194.
VMCAIVMCAI-2009-Emerson #problem
Model Checking: Progress and Problems (EAE), p. 1.
VMCAIVMCAI-2009-GallowayLMS #file system #linux
Model-Checking the Linux Virtual File System (AG, GL, JTM, RS), pp. 74–88.
VMCAIVMCAI-2009-GodefroidP #ltl #revisited
LTL Generalized Model Checking Revisited (PG, NP), pp. 89–104.
VMCAIVMCAI-2009-Gupta #concurrent #source code
Model Checking Concurrent Programs (AG), p. 2.
VMCAIVMCAI-2009-Oshman #bound
An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking (RO), pp. 275–289.
VMCAIVMCAI-2009-WimmerBB #bound #generative #markov #using
Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking (RW, BB, BB), pp. 366–380.
CBSECBSE-2008-VarekovaC #component
Model Checking of Control-User Component-Based Parametrised Systems (PV, IC), pp. 146–162.
QoSAQoSA-2008-GallottiGMT #composition #predict #probability #quality
Quality Prediction of Service Compositions through Probabilistic Model Checking (SG, CG, RM, GT), pp. 119–134.
QoSAQoSA-2008-PlsekA #component #named
Carmen: Software Component Model Checker (AP, JA), pp. 71–85.
CSEETCSEET-2008-SalamahG #education #specification #using
A Technique for Using Model Checkers to Teach Formal Specifications (SS, AQG), pp. 181–188.
SCAMSCAM-2008-WangZZ #automation #detection #program analysis
Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking (LW, QZ, PZ), pp. 165–173.
ICALPICALP-B-2008-BouyerMOW #complexity #on the #realtime
On Expressiveness and Complexity in Real-Time Model Checking (PB, NM, JO, JW), pp. 124–135.
FMFM-2008-MateescuT #concurrent
A Model Checking Language for Concurrent Value-Passing Systems (RM, DT), pp. 148–164.
SEFMSEFM-2008-EdelkampS #ltl
Flash-Efficient LTL Model Checking with Minimal Counterexamples (SE, DS), pp. 73–82.
SEFMSEFM-2008-FranzleH #approximate #calculus #performance
Efficient Model Checking for Duration Calculus Based on Branching-Time Approximations (MF, MRH), pp. 63–72.
GT-VCGT-VC-2007-BaresiRRS08 #graph transformation #performance
An Efficient Solution for Model Checking Graph Transformation Systems (LB, VR, ATR, PS), pp. 3–21.
ICEISICEIS-ISAS1-2008-MoralesTPA #communication #composition #concept #verification
A Conceptual Scheme for Compositional Model-Checking Verification of Critical Communicating Systems (LEMM, MICT, MAP, KBA), pp. 86–93.
ICEISICEIS-J-2008-MoralesCPA #composition #verification
Compositional Model-Checking Verification of Critical Systems (LEMM, MIC, MAP, KBA), pp. 213–225.
SEKESEKE-2008-ParkK #automaton #bound #constraints #lts #using
Using Boolean Cardinality Constraint for LTS Bounded Model Checking (SP, GK), pp. 537–542.
SEKESEKE-2008-SloanK #towards #web #web service
Toward Model Checking Web Services Over the Web (JCS, TMK), pp. 519–524.
OOPSLAOOPSLA-2008-RobersonHDB #performance #type system
Efficient software model checking of soundness of type systems (MR, MH, PTD, CB), pp. 493–504.
TOOLSTOOLS-EUROPE-2008-ArthoLHT #performance
Efficient Model Checking of Networked Applications (CA, WL, MH, YT), pp. 22–40.
PLDIPLDI-2008-GuerraouiHJS #transaction
Model checking transactional memories (RG, TAH, BJ, VS), pp. 372–382.
PLDIPLDI-2008-MusuvathiQ
Fair stateless model checking (MM, SQ), pp. 362–371.
QAPLQAPL-2008-FaellaLS #linear #logic
Model Checking Quantitative Linear Time Logic (MF, AL, MS), pp. 61–77.
ASEASE-2008-HartKGCL08a #named #proving
PtYasm: Software Model Checking with Proof Templates (TEH, KK, AG, MC, DL), pp. 479–480.
ASEASE-2008-KimKK #memory management #satisfiability #testing
Unit Testing of Flash Memory Device Driver through a SAT-Based Model Checker (MK, YK, HK), pp. 198–207.
ASEASE-2008-PostSKG #abstract interpretation #bound
Reducing False Positives by Combining Abstract Interpretation and Bounded Model Checking (HP, CS, AK, TG), pp. 188–197.
ICSEICSE-2008-LongDG #experience #industrial
Experience applying the SPIN model checker to an industrial telecommunications system (BL, JD, TCNG), pp. 693–702.
DACDAC-2008-MohalikRDRSPJ #analysis #embedded #latency #realtime
Model checking based analysis of end-to-end latency in embedded, real-time systems with clock drifts (SM, ACR, MGD, SR, PVS, PKP, SJ), pp. 296–299.
DATEDATE-2008-SteinhorstH #specification #using
Model Checking of Analog Systems using an Analog Specification Language (SS, LH), pp. 324–329.
PPoPPPPoPP-2008-VakkalankaSGK #named #source code
ISP: a tool for model checking MPI programs (SSV, SS, GG, RMK), pp. 285–286.
FASEFASE-2008-FantechiGLMPT #approach #specification #verification
A Model Checking Approach for Verifying COWS Specifications (AF, SG, AL, FM, RP, FT), pp. 230–245.
FoSSaCSFoSSaCS-2008-ChatterjeeSH #markov
Model-Checking ω-Regular Properties of Interval Markov Chains (KC, KS, TAH), pp. 302–317.
FoSSaCSFoSSaCS-2008-DemriLS #automaton #ltl
Model Checking Freeze LTL over One-Counter Automata (SD, RL, AS), pp. 490–504.
TACASTACAS-2008-BakewellG #game studies #on the fly
On-the-Fly Techniques for Game-Based Software Model Checking (AB, DRG), pp. 78–92.
TACASTACAS-2008-BarnatBSW #ltl
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking (JB, LB, PS, MW), pp. 48–62.
TACASTACAS-2008-CaniartFLZ
Accelerating Interpolation-Based Model-Checking (NC, EF, JL, MZ), pp. 428–442.
TACASTACAS-2008-ClarkeTV #abstraction #concurrent #framework #proving
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems (EMC, MT, HV), pp. 33–47.
TACASTACAS-2008-FinkbeinerPS #composition #named #synthesis
RESY: Requirement Synthesis for Compositional Model Checking (BF, HJP, SS), pp. 463–466.
TACASTACAS-2008-KatzP #programming #search-based
Model Checking-Based Genetic Programming with an Application to Mutual Exclusion (GK, DP), pp. 141–156.
TACASTACAS-2008-KupferschmidHL #abstraction #performance
Fast Directed Model Checking Via Russian Doll Abstraction (SK, JH, KGL), pp. 203–217.
TACASTACAS-2008-PaceS #visualisation
Computation and Visualisation of Phase Portraits for Model Checking SPDIs (GJP, GS), pp. 341–345.
TACASTACAS-2008-SankaranarayananDI #hybrid #using
Symbolic Model Checking of Hybrid Systems Using Template Polyhedra (SS, TD, FI), pp. 188–202.
TACASTACAS-2008-WulfDMR #algorithm #anti #ltl #named #satisfiability
Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking (MDW, LD, NM, JFR), pp. 63–77.
CAVCAV-2008-Bjesse #approach #industrial #word
A Practical Approach to Word Level Model Checking of Industrial Netlists (PB), pp. 446–458.
CAVCAV-2008-EdelkampSS #ltl
Semi-external LTL Model Checking (SE, PS, PS), pp. 530–542.
CAVCAV-2008-GayNP #named #quantum
QMC: A Model Checker for Quantum Systems (SJG, RN, NP), pp. 543–547.
CAVCAV-2008-Legay
T(O)RMC: A Tool for (ω)-Regular Model Checking (AL), pp. 548–551.
CAVCAV-2008-NiebertPP
Discriminative Model Checking (PN, DP, AP), pp. 504–516.
ICLPICLP-2008-Tsitovich #detection #security #using
Detection of Security Vulnerabilities Using Guided Model Checking (AT), pp. 822–823.
ICSTICST-2008-KimCKK
Pre-testing Flash Device Driver through Model Checking Techniques (MK, YC, YK, HK), pp. 475–484.
IJCARIJCAR-2008-GhilardiNRZ #smt #towards
Towards SMT Model Checking of Array-Based Systems (SG, EN, SR, DZ), pp. 67–82.
LICSLICS-2008-BaierBBBG #automaton #infinity
Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata (CB, NB, PB, TB, MG), pp. 217–226.
VMCAIVMCAI-2008-DSilvaPK #approximate #refinement
Approximation Refinement for Interpolation-Based Model Checking (VD, MP, DK), pp. 68–82.
VMCAIVMCAI-2008-FecherH #abstraction
Model Checking for Action Abstraction (HF, MH), pp. 112–126.
VMCAIVMCAI-2008-GroceJ #dynamic analysis
Extending Model Checking with Dynamic Analysis (AG, RJ), pp. 142–156.
CIAACIAA-2007-Vardi #automaton #linear
Linear-Time Model Checking: Automata Theory in Practice (MYV), pp. 5–10.
ICALPICALP-2007-TorreP #complexity #on the #recursion #state machine
On the Complexity of LtlModel-Checking of Recursive State Machines (SLT, GP), pp. 937–948.
LATALATA-2007-TabakovV #specification
Model Checking Buechi Specifications (DT, MYV), pp. 565–576.
IFMIFM-2007-PlaggeL #specification #using #validation
Validating Z Specifications Using the ProBAnimator and Model Checker (DP, ML), pp. 480–500.
RTARTA-2007-EscobarM #infinity #using
Symbolic Model Checking of Infinite-State Systems Using Narrowing (SE, JM), pp. 153–168.
SEFMSEFM-2007-PernaG #specification
Model Checking RAISE Applicative Specifications (JIP, CG), pp. 257–268.
SEFMSEFM-2007-RungtaM #benchmark #metric
Hardness for Explicit State Software Model Checking Benchmarks (NR, EGM), pp. 247–256.
SFMSFM-2007-KwiatkowskaNP #probability
Stochastic Model Checking (MZK, GN, DP), pp. 220–270.
ICFPICFP-2007-FredlundS #distributed #functional #named #programming language
McErlang: a model checker for a distributed functional programming language (LÅF, HS), pp. 125–136.
EDOCEDOC-2007-HalleVCG #workflow
Model Checking Data-Aware Workflow Properties with CTL-FO+ (SH, RV, OC, BG), pp. 267–278.
PADLPADL-2007-PodelskiR #abstraction #logic #named #refinement
ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement (AP, AR), pp. 245–259.
PPDPPPDP-2007-CheneyM
Mechanized metatheory model-checking (JC, AM), pp. 75–86.
ASEASE-2007-ArmandoBCMS
The eureka tool for software model checking (AA, MB, DC, JM, PS), pp. 541–542.
ASEASE-2007-KuHCL #benchmark #metric
A buffer overflow benchmark for software model checkers (KK, TEH, MC, DL), pp. 389–392.
ASEASE-2007-TkachukR #composition #generative #slicing
Combining environment generation and slicing for modular software model checking (OT, SPR), pp. 401–404.
ASEASE-2007-WitkowskiBKW #concurrent #linux
Model checking concurrent linux device drivers (TW, NB, DK, GW), pp. 501–504.
ESEC-FSEESEC-FSE-2007-FosterEKMRU #composition #constraints
Model checking service compositions under resource constraints (HF, WE, JK, JM, DSR, SU), pp. 225–234.
SACSAC-2007-FerreiraLO #approach #java
A Java code annotation approach for model checking software systems (GF, EL, EASO), pp. 1536–1537.
SACSAC-2007-OliveiraAS #component #formal method #modelling #petri net #using #verification
Formal modelling and verification of a component model using coloured petri nets and model checking (EASO, HOdA, LDdS), pp. 1427–1431.
DACDAC-2007-GuHY #distributed #embedded #optimisation
Optimization of Static Task and Bus Access Schedules for Time-Triggered Distributed Embedded Systems with Model-Checking (ZG, XH, MY), pp. 294–299.
DATEDATE-2007-CabodiNQ #induction #invariant
Boosting the role of inductive invariants in model checking (GC, SN, SQ), pp. 1319–1324.
DATEDATE-2007-GrosseKD #bound #functional
Estimating functional coverage in bounded model checking (DG, UK, RD), pp. 1176–1181.
WRLAWRLA-2006-NeuhausserN07 #abstraction #erlang #maude #source code
Abstraction and Model Checking of Core Erlang Programs in Maude (MRN, TN), pp. 147–163.
FoSSaCSFoSSaCS-2007-BouyerLM #automaton
Model-Checking One-Clock Priced Timed Automata (PB, KGL, NM), pp. 108–122.
TACASTACAS-2007-AbdullaDHR #performance #transducer #verification
Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems) (PAA, GD, NBH, AR), pp. 721–736.
TACASTACAS-2007-AlurCC
Model Checking on Trees with Path Equivalences (RA, PC, SC), pp. 664–678.
TACASTACAS-2007-AmlaM #abstraction #refinement #satisfiability
Combining Abstraction Refinement and SAT-Based Model Checking (NA, KLM), pp. 405–419.
TACASTACAS-2007-BattBW #liveness #network #search-based
Model Checking Liveness Properties of Genetic Regulatory Networks (GB, CB, RW), pp. 323–338.
TACASTACAS-2007-DoyenR #algorithm #approach
Improved Algorithms for the Automata-Based Approach to Model-Checking (LD, JFR), pp. 451–465.
TACASTACAS-2007-EtessamiKVY #markov #multi #process
Multi-objective Model Checking of Markov Decision Processes (KE, MZK, MYV, MY), pp. 50–65.
TACASTACAS-2007-HanK #probability
Counterexamples in Probabilistic Model Checking (TH, JPK), pp. 72–86.
TACASTACAS-2007-JurdzinskiLS #automaton #probability
Model Checking Probabilistic Timed Automata with One or Two Clocks (MJ, FL, JS), pp. 170–184.
TACASTACAS-2007-KatoenKZJ #bisimulation #probability
Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking (JPK, TK, ISZ, DNJ), pp. 87–101.
TACASTACAS-2007-KupferschmidDHFDPB #heuristic
Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking (SK, KD, JH, BF, HD, AP, GB), pp. 679–682.
AMOSTA-MOST-2007-FraserW #generative #ltl #performance #testing #using
Using LTL rewriting to improve the performance of model-checker based test-case generation (GF, FW), pp. 64–74.
AMOSTA-MOST-2007-SatpathyR #abstraction #formal method #generative #modelling #refinement #testing
Test case generation from formal models through abstraction refinement and model checking (MS, SR), pp. 85–94.
AMOSTA-MOST-2007-WijesekeraASF #specification #testing
Relating counterexamples to test cases in CTL model checking specifications (DW, PA, LS, GF), pp. 75–84.
CADECADE-2007-BaeldeGMNT
The Bedwyr System for Model Checking over Syntactic Expressions (DB, AG, DM, GN, AT), pp. 391–397.
CADECADE-2007-GhilardiNRZ #infinity #satisfiability
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems (SG, EN, SR, DZ), pp. 362–378.
CADECADE-2007-PerezV #bound #effectiveness #encoding #logic #ltl
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic (JANP, AV), pp. 346–361.
CAVCAV-2007-BeyerHT #configuration management #convergence #program analysis #verification
Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis (DB, TAH, GT), pp. 504–518.
CAVCAV-2007-CharltonH #analysis #named #plugin
Hector: Software Model Checking with Cooperating Analysis Plugins (NC, MH), pp. 168–172.
CAVCAV-2007-JonssonS
Systematic Acceleration in Regular Model Checking (BJ, MS), pp. 131–144.
CAVCAV-2007-MatsliahS #approximate #encryption #random
Underapproximation for Model-Checking Based on Random Cryptographic Constructions (AM, OS), pp. 339–351.
CAVCAV-2007-Segelken #abstraction #automaton #hybrid #linear #modelling
Abstraction and Counterexample-Guided Construction of ω-Automata for Model Checking of Step-Discrete Linear Hybrid Models (MS), pp. 433–448.
CSLCSL-2007-Dawar #automaton #first-order #locality #logic
Model-Checking First-Order Logic: Automata and Locality (AD), p. 6.
ISSTAISSTA-2007-HughesB #composition #interface
Interface grammars for modular software model checking (GH, TB), pp. 39–49.
LICSLICS-2007-KahlerKT #encryption #infinity #protocol
Infinite State AMC-Model Checking for Cryptographic Protocols (DK, RK, TT), pp. 181–192.
MBTMBT-2007-BorodayPG #nondeterminism #question #testing
Can a Model Checker Generate Tests for Non-Deterministic Systems? (SB, AP, RG), pp. 3–19.
MBTMBT-2007-FraserAW #testing
Handling Model Changes: Regression Testing and Test-Suite Update with Model-Checkers (GF, BKA, FW), pp. 33–46.
MBTMBT-2007-RaimondiPB #testing
Testing Planning Domains (without Model Checkers) (FR, CP, GB), pp. 113–125.
TAPTAP-2007-Gargantini #detection #fault #testing #using
Using Model Checking to Generate Fault Detecting Tests (AG), pp. 189–206.
FATESTestCom-FATES-2007-GromovW #testing
Testing and Model-Checking Techniques for Diagnosis (MG, TACW), pp. 138–154.
VMCAIVMCAI-2007-McMillan
Interpolants and Symbolic Model Checking (KLM), pp. 89–90.
VMCAIVMCAI-2007-MightCS
Model Checking Via GammaCFA (MM, BC, OS), pp. 59–73.
VMCAIVMCAI-2007-Siegel #source code
Model Checking Nonblocking MPI Programs (SFS), pp. 44–58.
VMCAIVMCAI-2007-Vardi #formal method #revisited
Automata-Theoretic Model Checking Revisited (MYV), pp. 137–150.
CIAACIAA-2006-RoyC #finite #infinity
A Finite Union of DFAs in Symbolic Model Checking of Infinite Systems (SR, BC), pp. 277–278.
FMFM-2006-DonaldsonM #approximate #reduction #symmetry
Exact and Approximate Strategies for Symmetry Reduction in Model Checking (AFD, AM), pp. 541–556.
FMFM-2006-JohnstonWBSR #modelling #order #performance
Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking (WJ, KW, LvdB, PAS, PJR), pp. 524–540.
FMFM-2006-McIver #analysis #probability #refinement
Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems (AM), pp. 131–146.
FMFM-2006-PnueliZ #runtime #verification
PSL Model Checking and Run-Time Verification Via Testers (AP, AZ), pp. 573–586.
OOPSLAOOPSLA-2006-DargaB #data type #performance
Efficient software model checking of data structure properties (PTD, CB), pp. 363–382.
QAPLQAPL-2005-KwiatkowskaNP06 #analysis #probability
Quantitative Analysis With the Probabilistic Model Checker PRISM (MZK, GN, DP), pp. 5–31.
PADLPADL-2006-Wang #automation #verification
Automatic Verification of a Model Checker by Reflection (BYW), pp. 45–59.
PEPMPEPM-2006-LewisJ #analysis
A dead variable analysis for explicit model checking (ML, MJ), pp. 48–57.
SASSAS-2006-BouajjaniHRV #data type
Abstract Regular Tree Model Checking of Complex Dynamic Data Structures (AB, PH, AR, TV), pp. 52–70.
ASEASE-2006-ArthoG
Accurate Centralization for Applying Model Checking on Networked Applications (CA, PLG), pp. 177–188.
ASEASE-2006-LiuYR #library #using
Software Library Usage Pattern Extraction Using a Software Model Checker (CL, EY, DJR), pp. 301–304.
ASEASE-2006-RobbyDH #framework #using
Domain-specific Model Checking Using The Bogor Framework (R, MBD, JH), pp. 369–370.
ICSEICSE-2006-ChangJ #declarative #modelling #relational
Symbolic model checking of declarative relational models (FSHC, DJ), pp. 312–320.
SACSAC-2006-JaghooriMS #named
Modere: the model-checking engine of Rebeca (MMJ, AM, MS), pp. 1810–1815.
CCCC-2006-LamprechtMS #analysis #data flow
Data-Flow Analysis as Model Checking Within the jABC (ALL, TMS, BS), pp. 101–104.
DACDAC-2006-AwedhS #automation #bound #invariant
Automatic invariant strengthening to prove properties in bounded model checking (MA, FS), pp. 1073–1076.
DATEDATE-2006-DasBDC #design #question #what
What lies between design intent coverage and model checking? (SD, PB, PD, PPC), pp. 1217–1222.
TACASTACAS-2006-LiS #abstraction #bound #performance #refinement
Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking (BL, FS), pp. 227–241.
TACASTACAS-2006-LomuscioR #multi #named
MCMAS: A Model Checker for Multi-agent Systems (AL, FR), pp. 450–454.
TACASTACAS-2006-NiebertP #ltl #partial order #performance
Efficient Model Checking for LTL with Partial Order Snapshots (PN, DP), pp. 272–286.
TACASTACAS-2006-SenVA #markov #nondeterminism
Model-Checking Markov Chains in the Presence of Uncertainties (KS, MV, GA), pp. 394–410.
AMOSTA-MOST-J-2005-Robinson-MallettLMG06 #identification #using #verification
Extended state identification and verification using a model checker (CRM, PL, TM, UG), pp. 981–992.
CAVCAV-2006-BurckhardtAM #bound #case study #concurrent #data type #memory management #modelling
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study (SB, RA, MMKM), pp. 489–502.
CAVCAV-2006-GurfinkelWC #named #verification
Yasm: A Software Model-Checker for Verification and Refutation (AG, OW, MC), pp. 170–174.
CAVCAV-2006-HeljankoJKLL #automaton #bound
Bounded Model Checking for Weak Alternating Büchi Automata (KH, TAJ, MK, ML, TL), pp. 95–108.
CAVCAV-2006-KahlonGS #concurrent #on the fly #partial order #source code #transaction #using
Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions (VK, AG, NS), pp. 286–299.
CAVCAV-2006-KwiatkowskaNP #probability #reduction #symmetry
Symmetry Reduction for Probabilistic Model Checking (MZK, GN, DP), pp. 234–248.
CAVCAV-2006-LalR #automaton
Improving Pushdown System Model Checking (AL, TWR), pp. 343–357.
CAVCAV-2006-SenA #testing #tool support
CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools (KS, GA), pp. 419–423.
CAVCAV-2006-SenV #parallel #source code #thread
Model Checking Multithreaded Programs with Asynchronous Atomic Methods (KS, MV), pp. 300–314.
CSLCSL-2006-GollerL #infinity #logic
Infinite State Model-Checking of Propositional Dynamic Logics (SG, ML), pp. 349–364.
CSLCSL-2006-Kaiser #automation #game studies #quantifier
Game Quantification on Automatic Structures and Hierarchical Model Checking Games (LK), pp. 411–425.
FATESFATES-RV-2006-ErnitsKRV #generative #modelling #refinement #testing #using
Generating Tests from EFSM Models Using Guided Model Checking and Iterated Search Refinement (JPE, AK, KR, JV), pp. 85–99.
ISSTAISSTA-2006-SiegelMAC #execution #parallel #source code #symbolic computation #using #verification
Using model checking with symbolic execution to verify parallel numerical programs (SFS, AM, GSA, LAC), pp. 157–168.
LICSLICS-2006-KahlonG #approach #ltl #thread
An Automata-Theoretic Approach for Model Checking Threads for LTL Propert (VK, AG), pp. 101–110.
LICSLICS-2006-Ong #higher-order #on the #recursion
On Model-Checking Trees Generated by Higher-Order Recursion Schemes (CHLO), pp. 81–90.
LICSLICS-2006-VaraccaV #logic
Temporal Logics and Model Checking for Fairly Correct Systems (DV, HV), pp. 389–398.
VMCAIVMCAI-2006-Bozzelli #automaton #complexity
Complexity Results on Branching-Time Pushdown Model Checking (LB), pp. 65–79.
VMCAIVMCAI-2006-GurfinkelWC #abstraction
Systematic Construction of Abstractions for Model-Checking (AG, OW, MC), pp. 381–397.
VMCAIVMCAI-2006-HristovaL #algorithm #automaton #linear #logic
Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems (KH, YAL), pp. 190–206.
VMCAIVMCAI-2006-JabbarE #linear #parallel
Parallel External Directed Model Checking with Linear I/O (SJ, SE), pp. 237–251.
VMCAIVMCAI-2006-Younes #fault #probability
Error Control for Probabilistic Model Checking (HLSY), pp. 142–156.
SCAMSCAM-2005-HongLS #abstract interpretation #approach #slicing
Abstract Slicing: A New Approach to Program Slicing Based on Abstract Interpretation and Model Checking (HSH, IL, OS), pp. 25–34.
FMFM-2005-DonaldsonM #automation #detection #symmetry #using
Automatic Symmetry Detection for Model Checking Using Computational Group Theory (AFD, AM), pp. 481–496.
FMFM-2005-EislerSJSS #case study
Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications (SE, CS, BJ, GS, JS), pp. 533–536.
FMFM-2005-HoenickeM #process #specification
Model-Checking of Specifications Integrating Processes, Data and Time (JH, PM), pp. 465–480.
FMFM-2005-IyerSEJ #clustering #on the
On Partitioning and Symbolic Model Checking (SKI, DS, EAE, JJ), pp. 497–511.
FMFM-2005-WoodcockCF #semantics
Operational Semantics for Model Checking Circus (JW, AC, LF), pp. 237–252.
IFMIFM-2005-GodefroidK
Software Model Checking: Searching for Computations in the Abstract or the Concrete (PG, NK), pp. 20–32.
SEFMSEFM-2005-CeroneLC #analysis #formal method #human-computer #interactive #using
Formal Analysis of Human-computer Interaction using Model-checking (AC, PAL, SC), pp. 352–362.
SEKESEKE-2005-IzadiM #algorithm #calculus #performance #μ-calculus
An Efficient Model Checking Algorithm for a Fragment of μ-Calculus (MI, AMR), pp. 392–395.
SEKESEKE-2005-Wang #infinity #logic #specification
Specification of an Infinite-State Local Model Checker in Rewriting Logic (BYW), pp. 442–447.
QAPLQAPL-2004-AlpuenteGPV05 #source code
Abstract Model Checking of tccp programs (MA, MdMG, EP, AV), pp. 19–36.
PADLPADL-2005-YangDRS #compilation #mobile #performance #process
A Provably Correct Compiler for Efficient Model Checking of Mobile Processes (PY, YD, CRR, SAS), pp. 113–127.
POPLPOPL-2005-FlanaganG #partial order #reduction
Dynamic partial-order reduction for model checking software (CF, PG), pp. 110–121.
ASEASE-2005-HaydarBPS #web
Properties and scopes in web model checking (MH, SB, AP, HAS), pp. 400–404.
ASEASE-2005-RungtaM #heuristic
A context-sensitive structural heuristic for guided search model checking (NR, EGM), pp. 410–413.
SACSAC-2005-Arias-FisteusFK
Applying model checking to BPEL4WS business collaborations (JAF, LSF, CDK), pp. 826–830.
SACSAC-2005-BalsaraR #predict #search-based #using
Prediction of inherited and genetic mutations using the software model checker SPIN (ZB, SR), pp. 208–209.
DACDAC-2005-GanaiGA #safety #satisfiability
Beyond safety: customized SAT-based model checking (MKG, AG, PA), pp. 738–743.
DACDAC-2005-GeilenBS #data flow #graph #requirements
Minimising buffer requirements of synchronous dataflow graphs with model checking (MG, TB, SS), pp. 819–824.
DATEDATE-2005-CabodiCNQ #bound #quantifier #set
Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking (GC, MC, SN, SQ), pp. 688–689.
DATEDATE-2005-KatzHD #bound
Space-Efficient Bounded Model Checking (JK, ZH, ND), pp. 686–687.
DATEDATE-2005-WenzelRKP #clustering #context-free grammar #generative
utomatic Timing Model Generation by CFG Partitioning and Model Checking (IW, BR, RK, PPP), pp. 606–611.
PPoPPPPoPP-2005-ShachamSS #information management #scalability #using
Scaling model checking of dataraces using dynamic information (OS, MS, AS), pp. 107–118.
WRLAWRLA-2004-PalominoP05 #maude #proving
Proving VLRL Action Properties with the Maude Model Checker (MP, IP), pp. 113–133.
WRLAWRLA-2004-Wang05 #calculus #maude #μ-calculus
μ-Calculus Model Checking in Maude (BYW), pp. 135–152.
ESOPESOP-2005-NaikP #type system
A Type System Equivalent to a Model Checker (MN, JP), pp. 374–388.
FoSSaCSFoSSaCS-2005-FerrariMT #calculus
Model Checking for Nominal Calculi (GLF, UM, ET), pp. 1–24.
FoSSaCSFoSSaCS-2005-LaroussinieS #probability
Model Checking Durational Probabilistic Systems (FL, JS), pp. 140–154.
TACASTACAS-2005-BaoJ
Time-Efficient Model Checking with Magnetic Disk (TB, MDJ), pp. 526–540.
TACASTACAS-2005-BouajjaniHMV #source code #verification
Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking (AB, PH, PM, TV), pp. 13–29.
TACASTACAS-2005-GanaiGA #framework #named #platform #satisfiability #scalability #verification
DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems (MKG, AG, PA), pp. 575–580.
TACASTACAS-2005-GrosuS #monte carlo
Monte Carlo Model Checking (RG, SAS), pp. 271–286.
TACASTACAS-2005-HammerKM #ltl #on the fly
Truly On-the-Fly LTL Model Checking (MH, AK, SM), pp. 191–205.
TACASTACAS-2005-KellerSBS #c #debugging #named #source code
FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs (CWK, DS, SB, SAS), pp. 563–569.
TACASTACAS-2005-McMillan
Applications of Craig Interpolants in Model Checking (KLM), pp. 1–12.
TACASTACAS-2005-QadeerR #bound #concurrent
Context-Bounded Model Checking of Concurrent Software (SQ, JR), pp. 93–107.
TACASTACAS-2005-RemkeHC #infinity #markov
Model Checking Infinite-State Markov Chains (AR, BRH, LC), pp. 237–252.
TACASTACAS-2005-SchuppanB #ltl
Shortest Counterexamples for Symbolic Model Checking of LTL with Past (VS, AB), pp. 493–509.
AMOSTA-MOST-2005-Robinson-MallettLMG #generative #sequence
Generating optimal distinguishing sequences with a model checker (CRM, PL, TM, UG), pp. 51–57.
CAVCAV-2005-BalakrishnanRKLLMGYCT #bytecode
Model Checking x86 Executables with CodeSurfer/x86 and WPDS++ (GB, TWR, NK, AL, JL, DM, RG, SHY, CHC, TT), pp. 158–163.
CAVCAV-2005-DwyerHHR #framework #using
Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework (MBD, JH, MH, R), pp. 148–152.
CAVCAV-2005-GuptaS #abstraction #bound #refinement
Abstraction Refinement for Bounded Model Checking (AG, OS), pp. 112–124.
CAVCAV-2005-HeljankoJL #bound #incremental
Incremental and Complete Bounded Model Checking for Full PLTL (KH, TAJ, TL), pp. 98–111.
CAVCAV-2005-PasareanuPV #refinement
Concrete Model Checking with Abstract Matching and Refinement (CSP, RP, WV), pp. 52–66.
CAVCAV-2005-PiazzaAMPWM #algebra #algorithm #biology #challenge
Algorithmic Algebraic Model Checking I: Challenges from Systems Biology (CP, MA, VM, AP, FW, BM), pp. 5–19.
CAVCAV-2005-RabinovitzG #bound #concurrent #source code
Bounded Model Checking of Concurrent Programs (IR, OG), pp. 82–97.
CAVCAV-2005-SebastianiTV #hybrid #ltl
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking (RS, ST, MYV), pp. 350–363.
CAVCAV-2005-SenVA #on the #probability #statistics
On Statistical Model Checking of Stochastic Systems (KS, MV, GA), pp. 266–280.
CAVCAV-2005-TangMGI #reduction #satisfiability #symmetry
Symmetry Reduction in SAT-Based Model Checking (DT, SM, AG, CNI), pp. 125–138.
CAVCAV-2005-Younes05a #named #statistics
Ymer: A Statistical Model Checker (HLSY), pp. 429–433.
CSLCSL-2005-CharatonikGM #bound #pointer #source code
Bounded Model Checking of Pointer Programs (WC, LG, PM), pp. 397–412.
ICLPICLP-2005-Mallya #deduction #multi
Deductive Multi-valued Model Checking (AM), pp. 297–310.
LICSLICS-2005-GodefroidH #logic #semantics
Model Checking Vs. Generalized Model Checking: Semantic Minimizations for Temporal Logics (PG, MH), pp. 158–167.
LICSLICS-2005-Lohrey
Model-Checking Hierarchical Structures (ML), pp. 168–177.
ICSTSAT-2005-DershowitzHK #bound
Bounded Model Checking with QBF (ND, ZH, JK), pp. 408–414.
ICSTSAT-2005-Zarpas #benchmark #bound #metric #satisfiability
Benchmarking SAT Solvers for Bounded Model Checking (EZ), pp. 340–354.
VMCAIVMCAI-2005-AbrahamBKS #bound #hybrid #linear #optimisation
Optimizing Bounded Model Checking for Linear Hybrid Systems (, BB, FK, MS), pp. 396–412.
VMCAIVMCAI-2005-Bozzelli #process #term rewriting
Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties (LB), pp. 282–297.
VMCAIVMCAI-2005-JabbarE #performance
I/O Efficient Directed Model Checking (SJ, SE), pp. 313–329.
VMCAIVMCAI-2005-LatvalaBHJ #bound #ltl #performance
Simple Is Better: Efficient Bounded Model Checking for Past LTL (TL, AB, KH, TAJ), pp. 380–395.
VMCAIVMCAI-2005-SistlaZW #commutative
Model Checking of Systems Employing Commutative Functions (APS, MZ, XW), pp. 250–266.
IWPCIWPC-2004-BeyerHJM #eclipse #plugin
An Eclipse Plug-in for Model Checking (DB, TAH, RJ, RM), pp. 251–255.
PASTEPASTE-2004-Godefroid
Invited Talk: “Model checking” software with VeriSoft (PG), p. 36.
ICALPICALP-2004-BrunsG #logic #multi
Model Checking with Multi-valued Logics (GB, PG), pp. 281–293.
IFMIFM-2004-ChakiCOSS
State/Event-Based Software Model Checking (SC, EMC, JO, NS, NS), pp. 128–147.
IFMIFM-2004-Melham #functional #proving #theorem proving
Integrating Model Checking and Theorem Proving in a Reflective Functional Language (TFM), pp. 36–39.
SEFMSEFM-2004-HamonMR #generative #performance #testing
Generating Efficient Test Sets with a Model Checker (GH, LMdM, JMR), pp. 261–270.
SEFMSEFM-2004-SchuleS #comparison #infinity #verification
Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems (TS, KS), pp. 67–76.
ICGTICGT-2004-RensinkSV #comparison #graph transformation
Model Checking Graph Transformations: A Comparison of Two Approaches (AR, ÁS, DV), pp. 226–241.
ICEISICEIS-v1-2004-Augusto #theorem proving #verification
Model Checking and Theorem Proving-Based Verification of EIS (JCA), p. XXXIII-XXXIV.
ICEISICEIS-v3-2004-StantonM #design #object-oriented
Model Checking an Object-Oriented Design (SCS, VMM), pp. 605–608.
KRKR-2004-EiterFFPW #bound #complexity #programming #set
Complexity of Model Checking and Bounded Predicate Arities for Non-ground Answer Set Programming (TE, WF, MF, GP, SW), pp. 377–387.
PPDPPPDP-2004-FarwerL #petri net #prolog
Model checking object petri nets in prolog (BF, ML), pp. 20–31.
ASEASE-2004-ChoiH #approach #case study
Combination Model Checking: Approach and a Case Study (YC, MPEH), pp. 354–357.
ASEASE-2004-DwyerRTV #interactive #order
Analyzing Interaction Orderings with Model Checking (MBD, R, OT, WV), pp. 154–163.
LDTALDTA-2004-GradaraSVV #modelling #parallel #source code #thread
Model Checking Multithreaded Programs by Means of Reduced Models (SG, AS, MLV, GV), pp. 55–74.
DACDAC-2004-WangJHS #bound #satisfiability
Refining the SAT decision ordering for bounded model checking (CW, HJ, GDH, FS), pp. 535–538.
DATEDATE-DF-2004-KruppMO #refinement
Formal Refinement and Model Checking of an Echo Cancellation Unit (AK, WM, IO), pp. 102–107.
OSDIOSDI-2004-YangTEM #fault #file system #using
Using Model Checking to Find Serious File System Errors (JY, PT, DRE, MM), pp. 273–288.
FASEFASE-2004-SaffreyC #communication #optimisation
Optimising Communication Structure for Model Checking (PS, MC), pp. 310–323.
FASEFASE-2004-XieLKB #design
Translating Software Designs for Model Checking (FX, VL, RPK, JCB), pp. 324–338.
TACASTACAS-2004-AlfaroFHMS
Model Checking Discounted Temporal Properties (LdA, MF, TAH, RM, MS), pp. 77–92.
TACASTACAS-2004-BoigelotLW
ω-Regular Model Checking (BB, AL, PW), pp. 561–575.
TACASTACAS-2004-Muller-OlmY #animation #game studies #named
MetaGame: An Animation Tool for Model-Checking Games (MMO, HY), pp. 163–167.
TACASTACAS-2004-QianN #abstraction #database #invariant
Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases (KQ, AN), pp. 497–511.
TACASTACAS-2004-RaviS #bound
Minimal Assignments for Bounded Model Checking (KR, FS), pp. 31–45.
TACASTACAS-2004-RobbyRDH #framework #specification #using
Checking Strong Specifications Using an Extensible Software Model Checking Framework (R, ER, MBD, JH), pp. 404–420.
TACASTACAS-2004-YounesKNP #empirical #probability #statistics
Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study (HLSY, MZK, GN, DP), pp. 46–60.
CAVCAV-2004-AbdullaJNdS #ltl
Regular Model Checking for LTL(MSO) (PAA, BJ, MN, Jd, MS), pp. 348–360.
CAVCAV-2004-AndrewsQRRX #concurrent #named
Zing: A Model Checker for Concurrent Software (TA, SQ, SKR, JR, YX), pp. 484–487.
CAVCAV-2004-AwedhS #bound #proving
Proving More Properties with Bounded Model Checking (MA, FS), pp. 96–108.
CAVCAV-2004-BouajjaniHV
Abstract Regular Model Checking (AB, PH, TV), pp. 372–386.
CAVCAV-2004-FinkelL #image #infinity
Image Computation in Infinite State Model Checking (AF, JL), pp. 361–371.
CAVCAV-2004-GammieM #logic #named
MCK: Model Checking the Logic of Knowledge (PG, RvdM), pp. 479–483.
CAVCAV-2004-GanaiGA #bound #embedded #modelling #performance
Efficient Modeling of Embedded Memories in Bounded Model Checking (MKG, AG, PA), pp. 440–452.
CAVCAV-2004-GoelB #abstraction #functional #order #simulation
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors (AG, REB), pp. 255–267.
CAVCAV-2004-GriffaultV
The Mec 5 Model-Checker (AG, AV), pp. 488–491.
CAVCAV-2004-JinAS #bound #named #satisfiability #towards
CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking (HJ, MA, FS), pp. 519–522.
CAVCAV-2004-Lange
Symbolic Model Checking of Non-regular Properties (ML), pp. 83–95.
CAVCAV-2004-Metzner #analysis #why
Why Model Checking Can Improve WCET Analysis (AM), pp. 334–347.
CAVCAV-2004-Namjoshi
An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking (KSN), pp. 57–69.
CAVCAV-2004-PitermanV #infinity
Global Model-Checking of Infinite-State Systems (NP, MYV), pp. 387–400.
CAVCAV-2004-SchroterK #parallel #petri net
Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings (CS, VK), pp. 109–121.
CAVCAV-2004-SebastianiSTV
GSTE Is Partitioned Model Checking (RS, ES, ST, MYV), pp. 229–241.
CAVCAV-2004-SenVA #black box #probability #statistics
Statistical Model Checking of Black-Box Probabilistic Systems (KS, MV, GA), pp. 202–215.
CAVCAV-2004-YangS #composition #specification
Compositional Specification and Model Checking in GSTE (JY, CJHS), pp. 216–228.
CSLCSL-2004-EmersonK #message passing
Parameterized Model Checking of Ring-Based Message Passing Systems (EAE, VK), pp. 325–339.
CSLCSL-2004-McMillan
Applications of Craig Interpolation to Model Checking (KLM), pp. 22–23.
FATESFATES-2004-HongU #cost analysis #generative #testing #using
Using Model Checking for Reducing the Cost of Test Generation (HSH, HU), pp. 110–124.
FATESFATES-2004-XieD #approach #component
An Automata-Theoretic Approach for Model-Checking Systems with Unspecified Components (GX, ZD), pp. 155–169.
LICSLICS-2004-DamsN #abstraction #branch #finite
The Existence of Finite Abstractions for Branching Time Model Checking (DD, KSN), pp. 335–344.
LICSLICS-2004-EsparzaKM #automaton #probability
Model Checking Probabilistic Pushdown Automata (JE, AK, RM), pp. 12–21.
LICSLICS-2004-FlumG #problem
Model-Checking Problems as a Basis for Parameterized Intractability (JF, MG), pp. 388–397.
LICSLICS-2004-WohrleT #infinity
Model Checking Synchronized Products of Infinite Transition Systems (SW, WT), pp. 2–11.
VMCAIVMCAI-2004-ClarkeKOS #bound #complexity
Completeness and Complexity of Bounded Model Checking (EMC, DK, JO, OS), pp. 85–96.
VMCAIVMCAI-2004-EnglerM #debugging #static analysis
Static Analysis versus Software Model Checking for Bug Finding (DRE, MM), pp. 191–210.
VMCAIVMCAI-2004-HatcliffRD #concurrent #object-oriented #specification #using #verification
Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking (JH, R, MBD), pp. 175–190.
VMCAIVMCAI-2004-HeraultLMP #approximate #probability
Approximate Probabilistic Model Checking (TH, RL, FM, SP), pp. 73–84.
VMCAIVMCAI-2004-LucanuC #algebra #specification
Model Checking for Object Specifications in Hidden Algebra (DL, GC), pp. 97–109.
VMCAIVMCAI-2004-PaceS #difference #kernel #using
Model Checking Polygonal Differential Inclusions Using Invariance Kernels (GJP, GS), pp. 110–121.
CSMRCSMR-2003-SciascioDMP #design #maintenance #using #web
Web Applications Design and Maintenance Using Symbolic Model Checking (EDS, FMD, MM, GP), pp. 63–72.
ICALPICALP-2003-Peled #testing
Model Checking and Testing Combined (DP), pp. 47–63.
ICALPICALP-2003-Schnoebelen
Oracle Circuits for Branching-Time Model Checking (PS), pp. 790–801.
FMFME-2003-ArmandoCG #analysis #graph #protocol #satisfiability #security #using
SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis (AA, LC, PG), pp. 875–893.
FMFME-2003-CompareIPS #analysis #architecture #lifecycle #validation
Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle (DC, PI, PP, AS), pp. 114–132.
FMFME-2003-GoldsmithMRWZ
Watchdog Transformations for Property-Oriented Model-Checking (MG, NM, BR, TW, IZ), pp. 600–616.
FMFME-2003-GurfinkelC #generative #multi
Generating Counterexamples for Multi-valued Model-Checking (AG, MC), pp. 503–521.
FMFME-2003-LeuschelB #named
ProB: A Model Checker for B (ML, MJB), pp. 855–874.
FMFME-2003-MorzentiPPS #specification
Model-Checking TRIO Specifications in SPIN (AM, MP, PSP, PS), pp. 542–561.
FMFME-2003-Schafer #analysis #fault #realtime
Combining Real-Time Model-Checking and Fault Tree Analysis (AS), pp. 522–541.
FMFME-2003-ThumsS
Model Checking FTA (AT, GS), pp. 739–757.
SEFMSEFM-2003-ShrotriBV #requirements #specification #visual notation
Model Checking Visual Specification of Requirements (US, PB, RV), pp. 202–209.
AGTIVEAGTIVE-2003-LaraGV #analysis #graph transformation #hybrid #metamodelling
Meta-Modelling, Graph Transformation and Model Checking for the Analysis of Hybrid Systems (JdL, EG, HV), pp. 292–298.
SEKESEKE-2003-OwenM #lightweight #named
Lurch: a Lightweight Alternative to Model Checking (DO, TM), pp. 158–165.
UMLUML-2003-SchmidtV #modelling #named #visual notation
CheckVML: A Tool for Model Checking Visual Modeling Languages (ÁS, DV), pp. 92–95.
ASEASE-2003-BarnatBC #ltl #parallel
Parallel Breadth-First Search LTL Model-Checking (JB, LB, JC), pp. 106–115.
ASEASE-2003-ChoiH #abstraction #reduction #requirements #specification #using
Model Checking Software Requirement Specifications using Domain Reduction Abstraction (YC, MPEH), pp. 314–317.
ASEASE-2003-TkachukDP #automation #generative
Automated Environment Generation for Software Model Checking (OT, MBD, CSP), pp. 116–129.
ESEC-FSEESEC-FSE-2003-GiannakopoulouM
Fluent model checking for event-based systems (DG, JM), pp. 257–266.
ESEC-FSEESEC-FSE-2003-RobbyDH #framework #named
Bogor: an extensible and highly-modular software model checking framework (R, MBD, JH), pp. 267–276.
ESEC-FSEESEC-FSE-2003-TkachukD #adaptation #analysis #composition
Adapting side effects analysis for modular program model checking (OT, MBD), pp. 188–197.
ICSEICSE-2003-EasterbrookCDGLPTT #multi #named #reasoning
χChek: A Model Checker for Multi-Valued Reasoning (SME, MC, BD, AG, AYCL, VP, AT, CDTW), pp. 804–805.
ICSEICSE-2003-HongCLSU #data flow #testing
Data Flow Testing as Model Checking (HSH, SDC, IL, OS, HU), pp. 232–243.
DACDAC-2003-ClarkeKY #behaviour #bound #c #consistency #source code #using
Behavioral consistency of C and verilog programs using bounded model checking (EMC, DK, KY), pp. 368–371.
DACDAC-2003-GuptaGWYA #bound #learning #satisfiability
Learning from BDDs in SAT-based bounded model checking (AG, MKG, CW, ZY, PA), pp. 824–829.
DACDAC-2003-KangP #bound #satisfiability
SAT-based unbounded symbolic model checking (HJK, ICP), pp. 840–843.
DACDAC-2003-TasiranYB #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-CabodiNQ #approximate #bound #satisfiability #traversal
Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals (GC, SN, SQ), pp. 10898–10905.
ESOPESOP-2003-Flanagan #automation #using
Automatic Software Model Checking Using CLP (CF), pp. 189–203.
FASEFASE-2003-SharyginaB #abstraction
Model Checking Software via Abstraction of Loop Transitions (NS, JCB), pp. 325–340.
FoSSaCSFoSSaCS-2003-BertrandS #decidability
Model Checking Lossy Channels Systems Is Probably Decidable (NB, PS), pp. 120–135.
TACASTACAS-2003-AmlaKMM #analysis #bound
Experimental Analysis of Different Techniques for Bounded Model Checking (NA, RPK, KLM, RM), pp. 34–48.
TACASTACAS-2003-BenedettiC #bound #ltl
Bounded Model Checking for Past LTL (MB, AC), pp. 18–33.
TACASTACAS-2003-EmersonK #agile #protocol
Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols (EAE, VK), pp. 144–159.
TACASTACAS-2003-KhurshidPV #execution #symbolic computation #testing
Generalized Symbolic Execution for Model Checking and Testing (SK, CSP, WV), pp. 553–568.
CADECADE-2003-Clarke #abstraction #refinement #satisfiability
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking (EMC), p. 1.
CAVCAV-2003-AbdullaJNd #algorithm
Algorithmic Improvements in Regular Model Checking (PAA, BJ, MN, Jd), pp. 236–248.
CAVCAV-2003-BartzisB #image #infinity #performance
Efficient Image Computation in Infinite State Model Checking (CB, TB), pp. 249–261.
CAVCAV-2003-BordiniFPVW #multi #source code
Model Checking Multi-Agent Programs with CASP (RHB, MF, CP, WV, MW), pp. 110–113.
CAVCAV-2003-CiardoS
Structural Symbolic CTL Model Checking of Asynchronous Systems (GC, RS), pp. 40–53.
CAVCAV-2003-DongRS #proving
Evidence Explorer: A Tool for Exploring Model-Checking Proofs (YD, CRR, SAS), pp. 215–218.
CAVCAV-2003-GlusmanK #consistency #specification
Model Checking Conformance with Scenario-Based Specifications (MG, SK), pp. 328–340.
CAVCAV-2003-McMillan #satisfiability
Interpolation and SAT-Based Model Checking (KLM), pp. 1–13.
CAVCAV-2003-MouraRS #bound #induction #verification
Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A) (LMdM, HR, MS), pp. 14–26.
CAVCAV-2003-Obdrzalek #bound #calculus #performance #μ-calculus
Fast μ-Calculus Model Checking when Tree-Width Is Bounded (JO), pp. 80–92.
CAVCAV-2003-SeshiaB #automaton #bound #using
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods (SAS, REB), pp. 154–166.
CSLCSL-2003-KahlerW #complexity #ltl
Program Complexity of Dynamic LTL Model Checking (DK, TW), pp. 271–284.
CSLCSL-2003-RybinaV #infinity #performance
Fast Infinite-State Model Checking in Integer-Based Systems (TR, AV), pp. 546–573.
FATESFATES-2003-HeimdahlRVDG #case study #sequence #testing #using
Auto-generating Test Sequences Using Model Checkers: A Case Study (MPEH, SR, WV, GD, JG), pp. 42–59.
ICLPICLP-2003-Fages
Symbolic Model-Checking for Biochemical Systems (FF), p. 102.
LICSLICS-2003-EmersonK #protocol
Model Checking Guarded Protocols (EAE, VK), pp. 361–370.
LICSLICS-2003-Kwiatkowska #probability #theory and practice
Model checking for probability and time: from theory to practice (MZK), p. 351–?.
LICSLICS-2003-Madhusudan
Model-checking Trace Event Structures (PM), pp. 371–380.
VMCAIVMCAI-2003-DamsN #abstraction #analysis
Shape Analysis through Predicate Abstraction and Model Checking (DD, KSN), pp. 310–324.
VMCAIVMCAI-2003-PnueliZ #abstraction
Model-Checking and Abstraction to the Aid of Parameterized Systems (AP, LDZ), p. 4.
VMCAIVMCAI-2003-Podelski #abstraction #refinement
Software Model Checking with Abstraction Refinement (AP), pp. 1–3.
VMCAIVMCAI-2003-Sistla #reduction #symmetry
Symmetry Reductions in Model-Checking (APS), p. 25.
VMCAIVMCAI-2003-YangRS #encoding #logic #mobile #process #using #π-calculus
A Logical Encoding of the pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution (PY, CRR, SAS), pp. 116–131.
ICALPICALP-2002-GenestMSZ #infinity
Infinite-State High-Level MSCs: Model-Checking and Realizability (BG, AM, HS, MZ), pp. 657–668.
FMFME-2002-HuberK #towards
Towards an Integrated Model Checker for Railway Signalling Data (MH, SK), pp. 204–223.
FMFME-2002-IoustinovaSS
Closing Open SDL-Systems for Model Checking with DTSpin (NI, NS, MS), pp. 531–548.
IFMIFM-2002-WinterD #using
Model Checking Object-Z Using ASM (KW, RD), pp. 165–184.
RTARTA-2002-DeharbeMR #logic
Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae (DD, AMM, CR), pp. 207–221.
CAiSECAiSE-2002-BenerecettiPST #multi #protocol #verification
Verification of Payment Protocols via MultiAgent Model Checking (MB, MP, LS, ST), pp. 311–327.
KRKR-2002-BaralZ #complexity
The Complexity of Model Checking for Knowledge Update (CB, YZ), pp. 82–96.
SEKESEKE-2002-HeDD #architecture #specification
Model checking software architecture specifications in SAM (XH, JD, YD), pp. 271–278.
SEKESEKE-2002-SantoneV #bytecode #java
Local model checking of Java bytecode (AS, GV), pp. 383–389.
POPLPOPL-2002-ChakiRR #message passing #modelling #source code
Types as models: model checking message-passing programs (SC, SKR, JR), pp. 45–57.
SASSAS-2002-GallardoMP #ltl #refinement
Refinement of LTL Formulas for Abstract Model Checking (MdMG, PM, EP), pp. 395–410.
SASSAS-2002-GiacobazziR #abstract interpretation
States vs. Traces in Model Checking by Abstract Interpretation (RG, FR), pp. 461–476.
SASSAS-2002-RanzatoT
Making Abstract Model Checking Strongly Preserving (FR, FT), pp. 411–427.
ASEASE-2002-Crhova #composition #distributed
Distributed Modular Model Checking (JC), p. 312.
ASEASE-2002-HeimdahlCW #analysis
Deviation Analysis Through Model Checking (MPEH, YC, MWW), pp. 37–46.
ASEASE-2002-LoerH #analysis #interactive #towards
Towards Usable and Relevant Model Checking Techniques for the Analysis of Dependable Interactive Systems (KL, MDH), pp. 223–226.
ICSEICSE-2002-ChandraGP #case study #industrial
Software model checking in practice: an industrial case study (SC, PG, CP), pp. 431–441.
ICSEICSE-2002-SchapachnikBO #approach #architecture #automaton #development #distributed
An architecture-centric approach to the development of a distributed model-checker for timed automata (FS, VAB, AO), p. 710.
SACSAC-2002-GallardoMMR #abstraction #using #xml
Using XML to implement abstraction for Model Checking (MdMG, JM, PM, ER), pp. 1021–1025.
DACDAC-2002-CabodiCQ #bound #question #satisfiability
Can BDDs compete with SAT solvers on bounded model checking? (GC, PC, SQ), pp. 117–122.
DACDAC-2002-HartongHB #algorithm #verification
Model checking algorithms for analog verification (WH, LH, EB), pp. 542–547.
DATEDATE-2002-HartongHB #approach
An Approach to Model Checking for Nonlinear Analog Systems (WH, LH, EB), p. 1080.
OSDIOSDI-2002-KumarL #debugging #using
Using Model Checking to Debug Device Firmware (SK, KL), pp. 61–74.
OSDIOSDI-2002-MusuvathiPCED #approach #named
CMC: A Pragmatic Approach to Model Checking Real Code (MM, DYWP, AC, DRE, DLD), pp. 75–88.
FASEFASE-2002-XieB #design #execution #object-oriented #reduction
Integrated State Space Reduction for Model Checking Executable Object-Oriented Software System Designs (FX, JCB), pp. 64–79.
FASEFASE-2002-XieLB #design #execution #named #object-oriented
ObjectCheck: A Model Checking Tool for Executable Object-Oriented Software System Designs (FX, VL, JCB), pp. 331–335.
FoSSaCSFoSSaCS-2002-LangeS #fixpoint #logic
Model Checking Fixed Point Logic with Chop (ML, CS), pp. 250–263.
FoSSaCSFoSSaCS-2002-LaroussinieMS #on the
On Model Checking Durational Kripke Structures (FL, NM, PS), pp. 264–279.
FoSSaCSFoSSaCS-2002-Loding #infinity
Model-Checking Infinite Systems Generated by Ground Tree Rewriting (CL), pp. 280–294.
TACASTACAS-2002-BallPR #abstraction #refinement
Relative Completeness of Abstraction Refinement for Software Model Checking (TB, AP, SKR), pp. 158–172.
TACASTACAS-2002-BasuKPR #recursion #source code
Resource-Constrained Model Checking of Recursive Programs (SB, KNK, LRP, CRR), pp. 236–250.
TACASTACAS-2002-EmersonK #resource management #scalability
Model Checking Large-Scale and Parameterized Resource Allocation Systems (EAE, VK), pp. 251–265.
TACASTACAS-2002-GrocePY #adaptation
Adaptive Model Checking (AG, DP, MY), pp. 357–370.
TACASTACAS-2002-KwiatkowskaNP #approach #hybrid #probability
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach (MZK, GN, DP), pp. 52–66.
TACASTACAS-2002-Mateescu #calculus #lts #μ-calculus
Local Model-Checking of Modal μ-Calculus on Acyclic Labeled Transition Systems (RM), pp. 281–295.
TACASTACAS-2002-Ouaknine #abstraction
Digitisation and Full Abstraction for Dense-Time Model Checking (JO), pp. 37–51.
WRLAWRLA-2002-EkerMS #ltl #maude
The Maude LTL Model Checker (SE, JM, AS), pp. 162–187.
CADECADE-2002-MouraRS #bound #infinity #lazy evaluation #proving #theorem proving
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains (LMdM, HR, MS), pp. 438–455.
CAVCAV-2002-AbdullaJMd
Regular Tree Model Checking (PAA, BJ, PM, Jd), pp. 555–568.
CAVCAV-2002-AlurMY #behaviour #performance
Exploiting Behavioral Hierarchy for Efficient Model Checking (RA, MM, ZY), pp. 338–342.
CAVCAV-2002-BarnerG #approximate #reduction #symmetry
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking (SB, OG), pp. 93–106.
CAVCAV-2002-BinghamH #bound
Semi-formal Bounded Model Checking (JDB, AJH), pp. 280–294.
CAVCAV-2002-ChatterjeeSG #consistency #memory management #modelling #protocol #refinement #verification
Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking (PC, HS, GG), pp. 123–136.
CAVCAV-2002-ChechikGD #multi #named
chi-Chek: A Multi-valued Model-Checker (MC, AG, BD), pp. 505–509.
CAVCAV-2002-CimattiCGGPRST
NuSMV 2: An OpenSource Tool for Symbolic Model Checking (AC, EMC, EG, FG, MP, MR, RS, AT), pp. 359–364.
CAVCAV-2002-GodefroidJ #abstraction #automation #using
Automatic Abstraction Using Generalized Model Checking (PG, RJ), pp. 137–150.
CAVCAV-2002-GrocePY #adaptation #named
AMC: An Adaptive Model Checker (AG, DP, MY), pp. 521–525.
CAVCAV-2002-HartongHB #modelling #on the
On Discrete Modeling and Model Checking for Nonlinear Analog Systems (WH, LH, EB), pp. 401–413.
CAVCAV-2002-Holzmann #analysis
Software Analysis and Model Checking (GJH), pp. 1–16.
CAVCAV-2002-Jacobi #pipes and filters #verification
Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving (CJ0), pp. 309–323.
CAVCAV-2002-KupfermanPV #linear
Model Checking Linear Properties of Prefix-Recognizable Systems (OK, NP, MYV), pp. 371–385.
CAVCAV-2002-KurshanLY
Compressing Transitions for Model Checking (RPK, VL, HY), pp. 569–581.
CAVCAV-2002-McMillan #bound #satisfiability
Applying SAT Methods in Unbounded Symbolic Model Checking (KLM), pp. 250–264.
CAVCAV-2002-RybinaV #canonical #infinity #using
Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking (TR, AV), pp. 386–400.
CAVCAV-2002-TanC
Evidence-Based Model Checking (LT, RC), pp. 455–470.
CSLCSL-2002-BeauquierRS #decidability #logic #probability
A Logic of Probability with Decidable Model-Checking (DB, AMR, AS), pp. 306–321.
ICLPICLP-2002-CharatonikMP #constraints #infinity
Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP (WC, SM, AP), pp. 115–129.
ICLPICLP-2002-PemmasaniRR #constraints #logic programming #performance #realtime #using
Efficient Real-Time Model Checking Using Tabled Logic Programming and Constraints (GP, CRR, IVR), pp. 100–114.
ISSTAISSTA-2002-GroceV #heuristic #java #source code #using
Model checking Java programs using structural heuristics (AG, WV), pp. 12–21.
LICSLICS-2002-ClarkeJLV
Tree-Like Counterexamples in Model Checking (EMC, SJ, YL, HV), pp. 19–29.
LICSLICS-2002-LaplanteLMPR #abstraction #approach #probability #testing
Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing (SL, RL, FM, SP, MdR), pp. 30–39.
SATSAT-2002-Clarke #abstraction #logic #refinement #satisfiability
SAT based abstraction refinement in temporal logic model checking (EC), p. 26.
VMCAIVMCAI-2002-BernardeschiF #abstract interpretation #bytecode #java #security
Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode (CB, NDF), pp. 1–15.
VMCAIVMCAI-2002-CimattiPRS #encoding #ltl #satisfiability
Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.
VMCAIVMCAI-2002-Huth #using
Model Checking Modal Transition Systems Using Kripke Structures (MH), pp. 302–316.
VMCAIVMCAI-2002-SidorovaS
Synchronous Closing of Timed SDL Systems for Model Checking (NS, MS), pp. 79–93.
ICALPICALP-2001-BenediktGR #state machine #strict
Model Checking of Unrestricted Hierarchical State Machines (MB, PG, TWR), pp. 652–666.
ICALPICALP-2001-GottlobP #clique
Hypergraphs in Model Checking: Acyclicity and Hypertree-Width versus Clique-Width (GG, RP), pp. 708–719.
FMFME-2001-ChechikEP #logic #multi
Model-Checking over Multi-valued Logics (MC, SME, VP), pp. 72–98.
FMFME-2001-LeuschelMC #csp #how #ltl #refinement
How to Make FDR Spin LTL Model Checking of CSP by Refinement (ML, TM, AC), pp. 99–118.
SEKESEKE-2001-BarberGH #architecture #correctness #simulation #using
Evaluating Dynamic Correctness Properties of Domain Reference Architectures Using a Combination of Simulation and Model Checking (KSB, TJG, JH), pp. 19–28.
LOPSTRLOPSTR-2001-LeuschelG #deduction #using
Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking (ML, SG), pp. 91–110.
PADLPADL-2001-Kaser #generative
State Generation in the PARMC Model Checker (OK), pp. 337–352.
PADLPADL-2001-Ramakrishnan #calculus #logic programming #using #μ-calculus
A Model Checker for Value-Passing μ-Calculus Using Logic Programming (CRR), pp. 1–13.
PPDPPPDP-2001-Esparza #declarative #source code
Model Checking (with) Declarative Programs (JE), p. 37.
SASSAS-2001-GiacobazziQ
Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking (RG, EQ), pp. 356–373.
RERE-2001-FuxmanMPT #requirements #specification
Model Checking Early Requirements Specifications in Tropos (AF, JM, MP, PT), pp. 174–181.
ASEASE-2001-BarberGH #architecture #automation #development #feedback
Providing Early Feedback in the Development Cycle Through Automated Application of Model Checking to Software Architectures (KSB, TJG, JH), pp. 341–345.
ASEASE-2001-BratV #static analysis
Combining Static Analysis and Model Checking for Software Analysis (GPB, WV), p. 262–?.
ASEASE-2001-Iosif #symmetry
Exploiting Heap Symmetries in Explicit-State Model Checking of Software (RI), pp. 254–261.
ASEASE-2001-Romanovsky #concurrent #realtime
Model-Checking Real-Time Concurrent Systems (IR), p. 439.
ASEASE-2001-XieLB #execution #set #uml
Model Checking for an Executable Subset of UML (FX, VL, JCB), pp. 333–336.
FSEESEC-FSE-2001-ChoiRH #abstraction #automation #constraints
Automatic abstraction for model checking software systems with interrelated numeric constraints (YC, SR, MPEH), pp. 164–174.
ICSEICSE-2001-AlurAGHKKMMW #design #named
JMOCHA: A Model Checking Tool that Exploits Design Structure (RA, LdA, RG, TAH, MK, CMK, RM, FYCM, BYW), pp. 835–836.
ICSEICSE-2001-Kaveh #design
Model Checking Distributd Objects Design (NK), pp. 793–794.
CCCC-2001-MartenaP #alias #analysis
Alias Analysis by Means of a Model Checker (VM, PSP), pp. 3–19.
DACDAC-2001-ChoiYLR #embedded #industrial
Model Checking of S3C2400X Industrial Embedded SOC Product (HC, BWY, YTL, HR), pp. 611–616.
FASEFASE-J-1998-MotaS01 #industrial #tool support
Model-checking CSP-Z: strategy, tool support and industrial application (AM, AS), pp. 59–96.
ESOPESOP-2001-Ranzato #on the
On the Completeness of Model Checking (FR), pp. 137–154.
FoSSaCSFoSSaCS-2001-CharatonikDGMT #complexity #mobile
The Complexity of Model Checking Mobile Ambients (WC, SDZ, ADG, SM, JMT), pp. 152–167.
FoSSaCSFoSSaCS-2001-LaroussinieMS
Model Checking CTL+ and FCTL is Hard (FL, NM, PS), pp. 318–331.
TACASTACAS-2001-BallPR #abstraction #c #source code
Boolean and Cartesian Abstraction for Model Checking C Programs (TB, AP, SKR), pp. 268–283.
TACASTACAS-2001-BolligLW #calculus #parallel #μ-calculus
Parallel Model Checking for the Alternation Free μ-Calculus (BB, ML, MW), pp. 543–558.
TACASTACAS-2001-ChechikDE #implementation #multi
Implementing a Multi-valued Symbolic Model Checker (MC, BD, SME), pp. 404–419.
TACASTACAS-2001-ChocklerKV #logic #metric
Coverage Metrics for Temporal Logic Model Checking (HC, OK, MYV), pp. 528–542.
TACASTACAS-2001-CimattiRB #automaton #set
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking (AC, MR, PB), pp. 313–327.
TACASTACAS-2001-HuneRSV #automaton #linear #parametricity
Linear Parametric Model Checking of Timed Automata (TH, JR, MS, FWV), pp. 189–203.
TACASTACAS-2001-Pandya
Model Checking CTL*[DC] (PKP), pp. 559–573.
TACASTACAS-2001-PasareanuDV #java #source code
Finding Feasible Counter-examples when Model Checking Abstracted Java Programs (CSP, MBD, WV), pp. 284–298.
TACASTACAS-2001-SebastianiTG #student
Model Checking Syllabi and Student Carreers (RS, AT, FG), pp. 128–142.
CAVCAV-2001-Alfaro #web
Model Checking the World Wide Web (LdA), pp. 337–349.
CAVCAV-2001-AmlaEKN #diagrams #named #performance
Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams (NA, EAE, RPK, KSN), pp. 387–390.
CAVCAV-2001-AsterothBA #modelling
Model Checking with Formula-Dependent Abstract Models (AA, CB, UA), pp. 155–168.
CAVCAV-2001-BhatCG #automaton #performance
Efficient Model Checking Via Büchi Tableau Automata (GB, RC, AG), pp. 38–52.
CAVCAV-2001-ChocklerKKV #approach
A Practical Approach to Coverage in Model Checking (HC, OK, RPK, MYV), pp. 66–78.
CAVCAV-2001-CoptyFFGKTV #bound #industrial
Benefits of Bounded Model Checking at an Industrial Setting (FC, LF, RF, EG, GK, AT, MYV), pp. 436–453.
CAVCAV-2001-EsparzaS #recursion #source code
A BDD-Based Model Checker for Recursive Programs (JE, SS), pp. 324–336.
CAVCAV-2001-GrumbergHS #calculus #distributed #μ-calculus
Distributed Symbolic Model Checking for μ-Calculus (OG, TH, AS), pp. 350–362.
CAVCAV-2001-JhalaM #architecture #composition #verification
Microarchitecture Verification by Compositional Model Checking (RJ, KLM), pp. 396–410.
CAVCAV-2001-LevinY #named
SDLcheck: A Model Checking Tool (VL, HY), p. 377.
CAVCAV-2001-Maidl #approach #safety
A Unifying Model Checking Approach for Safety Properties of Parameterized Systems (MM), pp. 311–323.
CAVCAV-2001-Namjoshi
Certifying Model Checkers (KSN), pp. 2–13.
CAVCAV-2001-ShanbhagGTAL #named
EASN: Integrating ASN.1 and Model Checking (VKS, KG, MT, AA, ML), pp. 382–386.
CAVCAV-2001-SistlaG #symmetry
Symmetry and Reduced Symmetry in Model Checking (APS, PG), pp. 91–103.
CSLCSL-2001-CharatonikT #decidability #mobile
The Decidability of Model Checking Mobile Ambients (WC, JMT), pp. 339–354.
ICALPICALP-2000-EsparzaH #approach #ltl
A New Unfolding Approach to LTL Model Checking (JE, KH), pp. 475–486.
IFMIFM-2000-HermannsKMS #algebra #probability #process #towards
Towards Model Checking Stochastic Process Algebra (HH, JPK, JMK, MS), pp. 420–439.
EDOCEDOC-2000-KaramanolisGMW #workflow
Model Checking of Workflow Schemas (CTK, DG, JM, SMW), pp. 170–181.
UMLUML-2000-Kwon #semantics #uml
Rewrite rules and Operational Semantics for Model Checking UML Statecharts (GK), pp. 528–540.
SASSAS-2000-Podelski #constraints #theorem proving
Model Checking as Constraint Solving (AP), pp. 22–37.
SASSAS-2000-Saidi #abstraction #analysis
Model Checking Guided Abstraction and Analysis (HS), pp. 377–396.
ASEASE-2000-ParkSSD #java
Java Model Checking (DYWP, US, JUS, DLD), pp. 253–256.
ASEASE-2000-VisserHBP #source code
Model Checking Programs (WV, KH, GPB, SP), pp. 3–12.
ICSEICSE-2000-Bultan #specification
Action Language: a specification language for model checking reactive systems (TB), pp. 335–344.
ICSEICSE-2000-CorbettDHR #interface #java #named #source code
Bandera: a source-level interface for model checking Java programs (JCC, MBD, JH, R), pp. 762–765.
ICSEICSE-2000-DangK #approximate #infinity #realtime
Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems (ZD, RAK), pp. 345–354.
DACDAC-2000-BloemRS
Symbolic guided search for CTL model checking (RB, KR, FS), pp. 29–34.
DACDAC-2000-YangT #lazy evaluation
Lazy symbolic model checking (JY, AT), pp. 35–38.
DATEDATE-2000-JangMH
Iterative Abstraction-Based CTL Model Checking (JYJ, IHM, GDH), pp. 502–507.
TACASTACAS-2000-AlfaroKNPS #probability #process #representation #using
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation (LdA, MZK, GN, DP, RS), pp. 395–410.
TACASTACAS-2000-BenerecettiG #logic #protocol #security #using
Model Checking Security Protocols Using a Logic of Belief (MB, FG), pp. 519–534.
TACASTACAS-2000-BosnackiDHS
Model Checking SDL with Spin (DB, DD, LH, NS), pp. 363–377.
TACASTACAS-2000-Bultan #concurrent #constraints #evaluation
BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems (TB), pp. 441–455.
TACASTACAS-2000-CastilloW
Model Checking Support for the ASM High-Level Language (GDC, KW), pp. 331–346.
TACASTACAS-2000-HenzingerM #hybrid
Symbolic Model Checking for Rectangular Hybrid Systems (TAH, RM), pp. 142–156.
TACASTACAS-2000-HermannsKMS #markov
A Markov Chain Model Checker (HH, JPK, JMK, MS), pp. 347–362.
TACASTACAS-2000-LarssonPY #on the #problem #traversal
On Memory-Block Traversal Problems in Model-Checking Timed-Systems (FL, PP, WY), pp. 127–141.
CADECADE-2000-EmersonK
Reducing Model Checking of the Many to the Few (EAE, VK), pp. 236–254.
CADECADE-2000-Seger #float #proving #theorem proving
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice (CJHS), p. 235.
CAVCAV-2000-BaierHHK #analysis #markov
Model Checking Continuous-Time Markov Chains by Transient Analysis (CB, BRH, HH, JPK), pp. 358–372.
CAVCAV-2000-BehrmannHV #how #matter #order
Distributing Timed Model Checking — How the Search Order Matters (GB, TH, FWV), pp. 216–231.
CAVCAV-2000-BouajjaniJNT
Regular Model Checking (AB, BJ, MN, TT), pp. 403–418.
CAVCAV-2000-CassezL #constraints #hybrid
Model-Checking for Hybrid Systems by Quotienting and Constraints Solving (FC, FL), pp. 373–388.
CAVCAV-2000-EsparzaHRS #algorithm #automaton #performance
Efficient Algorithms for Model Checking Pushdown Systems (JE, DH, PR, SS), pp. 232–247.
CAVCAV-2000-McMillanQS #composition #induction
Induction in Compositional Model Checking (KLM, SQ, JBS), pp. 312–327.
CAVCAV-2000-Shtrichman #bound #satisfiability
Tuning SAT Checkers for Bounded Model Checking (OS), pp. 480–494.
CAVCAV-2000-WilliamsBCG #diagrams #performance #satisfiability
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking (PFW, AB, EMC, AG), pp. 124–138.
ICLPCL-2000-BandaSHM
Model Checking in HAL (MJGdlB, PJS, WH, KM), pp. 1270–1284.
ICLPCL-2000-MukhopadhyayP #logic #process
Model Checking for Timed Logic Processes (SM, AP), pp. 598–612.
ICLPCL-2000-NilssonL #constraints #logic programming
Constraint Logic Programming for Local and Symbolic Model-Checking (UN, JL), pp. 384–398.
ICLPCL-2000-PettorossiP
Perfect Model Checking via Unfold/Fold Transformations (AP, MP), pp. 613–628.
ISSTAISSTA-2000-Dill #java #source code
Model checking Java programs (DLD), p. 179.
LICSLICS-2000-McMillan #proving #theorem
Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.
ICALPICALP-1999-DickhoferW #automaton #problem
Timed Alternating Tree Automata: The Automata-Theoretic Solution to the TCTL Model Checking Problem (MD, TW), pp. 281–290.
FMFM-v1-1999-BarbutiFSV #abstraction #realtime
Formula Based Abstractions of Transition Systems for Real-Time Model Checking (RB, NDF, AS, GV), pp. 289–306.
FMFM-v1-1999-Bousquet #case study #detection #experience #feature model #interactive #testing #using
Feature Interaction Detection Using Testing and Model-Checking Experience Report (LdB), pp. 622–641.
FMFM-v1-1999-DeharbeM #fixpoint
Symbolic Model Checking with Fewer Fixpoint Computations (DD, AMM), pp. 272–288.
FMFM-v1-1999-KestenKPR #analysis #deduction #verification
A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software (YK, AK, AP, GR), pp. 173–194.
FMFM-v1-1999-ReffelE #detection #fault
Error Detection with Directed Symbolic Model Checking (FR, SE), pp. 195–211.
FMFM-v2-1999-ButhS #architecture #communication #design
Model-Checking the Architectural Design of a Fail-Safe Communication System for Railway Interlocking Systems (BB, MS), p. 1869.
IFMIFM-1999-FischerW #specification
Model-Checking CSP-OZ Specifications with FDR (CF, HW), pp. 315–334.
IFMIFM-1999-ReedSG #deduction #development #formal method #reasoning
Deductive Reasoning versus Model Checking: Two Formal Approaches for System Development (JNR, JES, FG), pp. 375–394.
UMLUML-1999-PaltorL #formal method #state machine #uml
Formalising UML State Machines for Model Checking (IP, JL), pp. 430–445.
LOPSTRLOPSTR-1999-Fribourg #constraints #logic programming
Constraint Logic Programming Applied to Model Checking (LF), pp. 30–41.
LOPSTRLOPSTR-1999-LeuschelM #abstract interpretation #infinity
Infinite State Model Checking by Abstract Interpretation and Program Specialisation (ML, TM), pp. 62–81.
SASSAS-1999-Muller-OlmSS #named #tutorial
Model-Checking: A Tutorial Introduction (MMO, DAS, BS), pp. 330–354.
ESECESEC-FSE-1999-GargantiniH #requirements #specification #testing #using
Using Model Checking to Generate Tests from Requirements Specifications (AG, CLH), pp. 146–162.
ICSEICSE-1999-ChanABJNW #performance
Decoupling Synchronization from Local Control for Efficient Symbolic Model Checking of Statecharts (WC, RJA, PB, DHJ, DN, WEW), pp. 142–151.
ICSEICSE-1999-DangK #mobile #using
Using the ASTRAL Model Checker to Analyze Mobile IP (ZD, RAK), pp. 132–142.
DACDAC-1999-BiereCCFZ #satisfiability #using
Symbolic Model Checking Using SAT Procedures instead of BDDs (AB, AC, EMC, MF, YZ), pp. 317–320.
DACDAC-1999-HoskoteKHZ #estimation
Coverage Estimation for Symbolic Model Checking (YVH, TK, PHH, XZ), pp. 300–305.
DATEDATE-1999-MeinelS #order #performance
Increasing Efficiency of Symbolic Model Checking by Accelerating Dynamic Variable Reordering (CM, CS), pp. 760–761.
DATEDATE-1999-StrehlT #diagrams #petri net
Interval Diagram Techniques for Symbolic Model Checking of Petri Nets (KS, LT), pp. 756–757.
FoSSaCSFoSSaCS-1999-HuhnNW #communication #logic
Model Checking Logics for Communicating Sequential Agents (MH, PN, FW), pp. 227–242.
TACASTACAS-1999-BiereCCZ
Symbolic Model Checking without BDDs (AB, AC, EMC, YZ), pp. 193–207.
TACASTACAS-1999-DelzannoP
Model Checking in CLP (GD, AP), pp. 223–239.
CAVCAV-1999-BasinFPV #bytecode #java #verification
Java Bytecode Verification by Model Checking (DAB, SF, JP, HV), pp. 491–494.
CAVCAV-1999-BaumgartnerHSA #abstraction #algorithm
Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists (JB, TH, VS, AA), pp. 72–83.
CAVCAV-1999-BiereCRZ #safety #using
Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs (AB, EMC, RR, YZ), pp. 60–71.
CAVCAV-1999-BloemRS #linear #logic #performance
Efficient Decision Procedures for Model Checking of Linear Time Logic Properties (RB, KR, FS), pp. 222–235.
CAVCAV-1999-BoppanaRTF
Model Checking Based on Sequential ATPG (VB, SPR, KT, MF), pp. 418–430.
CAVCAV-1999-BrunsG #logic
Model Checking Partial State Spaces with 3-Valued Temporal Logics (GB, PG), pp. 274–287.
CAVCAV-1999-JeronM #generative #testing
Test Generation Derived from Model-Checking (TJ, PM), pp. 108–121.
CAVCAV-1999-KupfermanV #safety
Model Checking of Safety Properties (OK, MYV), pp. 172–183.
CAVCAV-1999-Lind-NielsenA
Stepwise CTL Model Checking of State/Event Systems (JLN, HRA), pp. 316–327.
CAVCAV-1999-ManoliosNS #bisimulation #proving #theorem proving
Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation (PM, KSN, RS), pp. 369–379.
CAVCAV-1999-YangSBO #constraints #modelling #optimisation
Optimizing Symbolic Model Checking for Constraint-Rich Models (BY, RGS, REB, DRO), pp. 328–340.
ICALPICALP-1998-Henzinger #game studies #multi
Model Checking Game Properties of Multi-agent Systems (TAH), p. 543.
FMFM-1998-FantechiGMPT
A Symbolic Model Checker for ACTL (AF, SG, FM, RP, ET), pp. 228–242.
KRKR-1998-CervesatoFM #calculus #complexity #quantifier
The Complexity of Model Checking in Modal Event Calculi with Quantifiers (IC, MF, AM), pp. 368–379.
PPDPALP-PLILP-1998-CuiDDKRRRSW #logic programming
Logic Programming and Model Checking (BC, YD, XD, KNK, CRR, IVR, AR, SAS, DSW), pp. 1–20.
POPLPOPL-1998-Schmidt #abstract interpretation #analysis #data flow
Data Flow Analysis is Model Checking of Abstract Interpretations (DAS), pp. 38–48.
SASSAS-1998-Levi #semantics
A Symbolic Semantics for Abstract Model Checking (FL), pp. 134–151.
SASSAS-1998-SchmidtS #abstract interpretation #program analysis
Program Analysis as Model Checking of Abstract Interpretations (DAS, BS), pp. 351–380.
REICRE-1998-SchneiderECH #fault tolerance #requirements #using #validation
Validating Requirements for Fault Tolerant Systems using Model Checking (FS, SME, JRC, GJH), pp. 4–13.
FSEFSE-1998-AlurY #state machine
Model Checking of Hierarchical State Machines (RA, MY), pp. 175–188.
FSEFSE-1998-DwyerP
Filter-Based Model Checking of Partial Systems (MBD, CSP), pp. 189–202.
DACDAC-1998-PardoH #incremental #using
Incremental CTL Model Checking Using BDD Subsetting (AP, GDH), pp. 457–462.
FASEFASE-1998-MotaS
Model-Checking CSP-Z (AM, AS), pp. 205–220.
TACASTACAS-1998-AcetoBL #automaton #reachability #testing
Model Checking via Reachability Testing for Timed Automata (LA, AB, KGL), pp. 263–280.
TACASTACAS-1998-AjamiHI #linear #logic #symmetry
Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond (KA, SH, JMI), pp. 52–67.
TACASTACAS-1998-DawsT #abstraction #reachability #realtime #using
Model Checking of Real-Time Reachability Properties Using Abstractions (CD, ST), pp. 313–329.
TACASTACAS-1998-LasterG #composition
Modular Model Checking of Software (KL, OG), pp. 20–35.
TACASTACAS-1998-Sprenger #calculus #coq #μ-calculus
A Verified Model Checker for the Modal μ-calculus in Coq (CS), pp. 167–183.
TACASTACAS-1998-StevensS #game studies #using
Practical Model-Checking Using Games (PS, CS), pp. 85–101.
CAVCAV-1998-AlurHMQRT #composition #named
MOCHA: Modularity in Model Checking (RA, TAH, FYCM, SQ, SKR, ST), pp. 521–525.
CAVCAV-1998-BeerBL #on the fly
On-the-Fly Model Checking of RCTL Formulas (IB, SBD, AL), pp. 184–194.
CAVCAV-1998-Bolignano #encryption #protocol #verification
Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols (DB), pp. 77–87.
CAVCAV-1998-BozgaDMOTY #named #realtime
Kronos: A Model-Checking Tool for Real-Time Systems (MB, CD, OM, AO, ST, SY), pp. 546–550.
CAVCAV-1998-ClarkeEJS #reduction #symmetry
Symmetry Reductions inModel Checking (EMC, EAE, SJ, APS), pp. 147–158.
CAVCAV-1998-Daws #named #realtime
Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems (CD), pp. 542–545.
CAVCAV-1998-HenzingerKQ
From Pre-historic to Post-modern Symbolic Model Checking (TAH, OK, SQ), pp. 195–206.
CAVCAV-1998-Holzmann #on the
On Checking Model Checkers (GJH), pp. 61–70.
CAVCAV-1998-KaufmannMP #constraints #design
Design Constraints in Symbolic Model Checking (MK, AM, CP), pp. 477–487.
CAVCAV-1998-MankuHB #symmetry
Structural Symmetry and Model Checking (GSM, RH, RKB), pp. 159–171.
CAVCAV-1998-McMillan #algorithm #composition #implementation #verification
Verification of an Implementation of Tomasulo’s Algorithm by Compositional Model Checking (KLM), pp. 110–121.
CAVCAV-1998-NalumasuGMG #approach #memory management #modelling #multi #verification
The “Test Model-Checking” Approach to the Verification of Formal Memory Models of Multiprocessors (RN, RG, AM, GG), pp. 464–476.
CAVCAV-1998-Wallner #ltl #using
Model Checking LTL Using Net Unforldings (FW), pp. 207–218.
CAVCAV-1998-XuCSCM #first-order #graph #logic #multi #using
Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs (YX, EC, XS, FC, OAM), pp. 219–231.
ISSTAISSTA-1998-ChanABN #performance #requirements
Improving Efficiency of Symbolic Model Checking for State-Based System Requirements (WC, RJA, PB, DN), pp. 102–112.
ISSTAISSTA-1998-GodefroidHJ #analysis #monitoring #using
Model Checking Without a Model: An Analysis of the Heart-Beat Monitor of a Telephone Switch Using VeriSoft (PG, RSH, LJJ), pp. 124–133.
LICSLICS-1998-EmersonN #infinity #nondeterminism #on the
On Model Checking for Non-Deterministic Infinite-State Systems (EAE, KSN), pp. 70–80.
ICALPICALP-1997-BaierCHKR #probability #process
Symbolic Model Checking for Probabilistic Processes (CB, EMC, VHG, MZK, MR), pp. 430–440.
ICALPICALP-1997-BurkartS #calculus #infinity #process #μ-calculus
Model Checking the Full Modal μ-Calculus for Infinite Sequential Processes (OB, BS), pp. 419–429.
FMFME-1997-YuL #implementation
Implementing a Model Checker for LEGO (SY, ZL), pp. 442–458.
POPLPOPL-1997-Godefroid #programming language #using
Model Checking for Programming Languages using Verisoft (PG), pp. 174–186.
ESECESEC-FSE-1997-DwyerCH #abstraction #user interface #using #visual notation
Model Checking Graphical User Interfaces Using Abstractions (MBD, VC, LH), pp. 244–261.
ICSEICSE-1997-AlurJKO #realtime
Model-Checking of Real-Time Systems: A Telecommunications Application (RA, LJJ, JJK, JVO), pp. 514–524.
DATEEDTC-1997-KropfR #using
Using MTBDDs for discrete timed symbolic model checking (TK, JR), pp. 182–187.
TACASTACAS-1997-AndersenSM
Partial Model Checking with ROBDDs (HRA, JS, NM), pp. 35–49.
TACASTACAS-1997-EngelsFM #generative #network #testing #using
Test Generation for Intelligent Networks Using Model Checking (AE, LMGF, SM), pp. 384–398.
TACASTACAS-1997-OwreRS #integration
Integration in PVS: Tables, Types, and Model Checking (SO, JMR, NS), pp. 366–383.
TACASTACAS-1997-Penczek #subclass
Model-Checking for a Subclass of Event Structures (WP), pp. 145–164.
TAPSOFTTAPSOFT-1997-BeauquierS #algorithm #problem #semantics #towards
The Railroad Crossing Problem: Towards Semantics of Timed Algorithms and Their Model Checking in High Level Languages (DB, AS), pp. 201–212.
TAPSOFTTAPSOFT-1997-IlieA #graph #reachability
Model Checking Through Symbolic Reachability Graph (JMI, KA), pp. 213–224.
CAVCAV-1997-BarrettM #design
Model Checking in a Microprocessor Design Project (GB, AM), pp. 214–225.
CAVCAV-1997-BeerBEGGHLPRRW #named
RuleBase: Model Checking at IBM (IB, SBD, CE, DG, LG, TH, AL, PP, YR, GR, YW), pp. 480–483.
CAVCAV-1997-Biere #calculus #named #performance #μ-calculus
μcke — Efficient μ-Calculus Model Checking (AB), pp. 468–471.
CAVCAV-1997-BultanGP #infinity #using
Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic (TB, RG, WP), pp. 400–411.
CAVCAV-1997-ChanABN #constraints #theorem proving
Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints (WC, RJA, PB, DN), pp. 316–327.
CAVCAV-1997-GyurisS #on the fly #symmetry
On-the-Fly Model Checking Under Fairness That Exploits Symmetry (VG, APS), pp. 232–243.
CAVCAV-1997-HenzingerHW #hybrid #named
HYTECH: A Model Checker for Hybrid Systems (TAH, PHH, HWT), pp. 460–463.
CAVCAV-1997-ImmermanV #logic #transitive
Model Checking and Transitive-Closure Logic (NI, MYV), pp. 291–302.
CAVCAV-1997-KestenMMPS
Symbolic Model Checking with Rich ssertional Languages (YK, OM, MM, AP, ES), pp. 424–435.
CAVCAV-1997-PardoH #abstraction #automation #calculus #μ-calculus
Automatic Abstraction Techniques for Propositional μ-calculus Model Checking (AP, GDH), pp. 12–23.
CAVCAV-1997-RamakrishnanRRSSW #performance #using
Efficient Model Checking Using Tabled Resolution (YSR, CRR, IVR, SAS, TS, DSW), pp. 143–154.
CAVCAV-1997-SistlaMG #liveness #named #symmetry #verification
SMC: A Symmetry Based Model Checker for Verification of Liveness Properties (APS, LM, VG), pp. 464–467.
ICLPICLP-1997-CervesatoFM #calculus #complexity
The Complexity of Model Checking in Modal Event Calculi (IC, MF, AM), p. 419.
ICLPILPS-1997-Clarke #logic
Temporal Logic Model Checking (EMC), p. 3.
ICLPILPS-1997-Gerth
Model Checking (RG), p. 39.
LICSLICS-1997-HuthK #analysis
Quantitative Analysis and Model Checking (MH, MZK), pp. 111–122.
FMFME-1996-BoigelotG #analysis #protocol #using
Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN (BB, PG), pp. 465–478.
FMFME-1996-HavelundS #protocol #proving #theorem proving #verification
Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.
FSEFSE-1996-AndersonBBCMNR #scalability #specification
Model Checking Large Software Specifications (RJA, PB, SB, WC, FM, DN, JDR), pp. 156–166.
DACDAC-1996-ClarkeKZ #fault #word
Word Level Model Checking — Avoiding the Pentium FDIV Error (EMC, MK, XZ), pp. 645–648.
TACASTACAS-1996-BhatC #calculus #μ-calculus
Efficent Local Model-Checking for Fragments of teh Modal μ-Calculus (GB, RC), pp. 107–126.
TACASTACAS-1996-ChouP #partial order #reduction #verification
Formal Verification of a Partial-Order Reduction Technique for Model Checking (CTC, DP), pp. 241–257.
CAVCAV-1996-Avrunin #algebra #geometry #using
Symbolic Model Checking Using Algebraic Geometry (GSA), pp. 26–37.
CAVCAV-1996-CamposG #analysis #verification
Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System (SVAC, OG), pp. 257–268.
CAVCAV-1996-ClarkeMCH
Symbolic Model Checking (EMC, KLM, SVAC, VHG), pp. 419–427.
CAVCAV-1996-McMillan #representation
A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking (KLM), pp. 13–25.
CAVCAV-1996-OwreRRSS #named #proving #specification
PVS: Combining Specification, Proof Checking, and Model Checking (SO, SR, JMR, NS, MKS), pp. 411–414.
CAVCAV-1996-ShuklaHR #game studies #verification
HORNSAT, Model Checking, Verification and games (SKS, HBHI, DJR), pp. 99–110.
CAVCAV-1996-SipmaUM #deduction
Deductive Model Checking (HS, TEU, ZM), pp. 208–219.
CAVCAV-1996-Walukiewicz #automaton #game studies #process
Pushdown Processes: Games and Model Checking (IW), pp. 62–74.
ISSTAISSTA-1996-BultanFG #composition #verification
Compositional Verification by Model Checking for Counter-Examples (TB, JF, RG), pp. 224–238.
LICSLICS-1996-AlurMP #concurrent #correctness
Model-Checking of Correctness Conditions for Concurrent Objects (RA, KLM, DP), pp. 219–228.
LICSLICS-1996-BhatC #calculus #equation #performance #μ-calculus
Efficient Model Checking via the Equational μ-Calculus (GB, RC), pp. 304–312.
LICSLICS-1996-WillemsW #branch #linear #partial order
Partial-Order Methods for Model Checking: From Linear Time to Branching Time (BW, PW), pp. 294–303.
SEKESEKE-1995-LinL #message passing #protocol #verification
Formal Verification of a Message-Passing Protocol with Model Checking (AL, FL), pp. 296–302.
PEPMPEPM-1995-Cridlig #analysis #concurrent #semantics #using
Semantic Analysis of Shared-Memory Concurrent Languages using Abstract Model-Checking (RC), pp. 214–225.
SASSAS-1995-CleavelandIY #abstraction
Optimality in Abstractions of Model Checking (RC, SPI, DY), pp. 51–63.
ESECESEC-1995-TuyaSC #modelling #safety #using #verification
Using a Symbolic Model Checker for Verify Safety Properties in SA/RT Models (JT, LS, JAC), pp. 59–75.
FSEFSE-1995-WingV #case study
Model Checking Software Systems: A Case Study (JMW, MV), pp. 128–139.
DACDAC-1995-BormannLPV #design #hardware #industrial
Model Checking in Industrial Hardware Design (JB, JL, MP, GV), pp. 298–303.
DACDAC-1995-ClarkeGMZ #generative #performance
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking (EMC, OG, KLM, XZ), pp. 427–432.
TACASTACAS-1995-FrancescoFGI #approximate #finite #process
Model Checking of Non-Finite State Processes by Finite Approximations (NDF, AF, SG, PI), pp. 195–215.
TACASTACAS-1995-Mader #calculus #μ-calculus
Modal μ-Calculus, Model Checking and Gauß Elimination (AM), pp. 72–88.
TACASTACAS-1995-MullerN #deduction
Combining Model Checking and Deduction for I/O-Automata (OM, TN), pp. 1–16.
TACASTACAS-1995-RoscoeGGHJS #concurrent #csp #how
Hierarchical Compression for Model-Checking CSP or How to Check 1020 Dining Philosophers for Deadlock (AWR, PHBG, MG, JRH, DMJ, JBS), pp. 133–152.
CAVCAV-1995-DingelF #abstraction #infinity #proving #reasoning #theorem proving #using
Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving (JD, TF), pp. 54–69.
CAVCAV-1995-Emerson #calculus #tutorial #μ-calculus
Methods for μ-calculus Model Checking: A Tutorial (EAE), p. 141.
CAVCAV-1995-EmersonS #approach #symmetry
Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach (EAE, APS), pp. 309–324.
CAVCAV-1995-EsparzaK #branch #logic #on the #parallel #problem #process
On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes (JE, AK), pp. 353–366.
CAVCAV-1995-RajanSS #automation #integration #proving
An Integration of Model Checking with Automated Proof Checking (SR, NS, MKS), pp. 84–97.
CAVCAV-1995-SokolskyS #realtime
Local Model Checking for Real-Time Systems (OS, SAS), pp. 211–224.
LICSLICS-1995-AlurPP
Model-Checking of Causality Properties (RA, DP, WP), pp. 90–100.
LICSLICS-1995-Andersen
Partial Model Checking (HRA), pp. 398–407.
LICSLICS-1995-BhatCG #on the fly #performance
Efficient On-the-Fly Model Checking for CTL* (GB, RC, OG), pp. 388–397.
LICSLICS-1995-Vardi #complexity #composition #on the
On the Complexity of Modular Model Checking (MYV), pp. 101–111.
FMFME-1994-Jackson #infinity #specification
Abstract Model Checking of Infinite Specifications (DJ), pp. 519–531.
DATEEDAC-1994-ChenYF #debugging #design #identification
Bug Identification of a Real Chip Design by Symbolic Model Checking (BC, MY, MF), pp. 132–136.
ESOPESOP-1994-CorsiniR #constraints #logic programming
Symbolic Model Checking and Constraint Logic Programming: a Cross-Fertilization (MMC, AR), pp. 180–194.
CAVCAV-1994-AzizSS #composition #equivalence
Formula-Dependent Equivalence for Compositional CTL Model Checking (AA, TRS, VS), pp. 324–337.
CAVCAV-1994-BernholtzVW #approach
An Automata-Theoretic Approach to Branching-Time Model Checking (OB, MYV, PW), pp. 142–155.
CAVCAV-1994-ClarkeGH #ltl
Another Look at LTL Model Checking (EMC, OG, KH), pp. 415–427.
CAVCAV-1994-DamsGDHKP #abstraction #adaptation #using
Model Checking Using Adaptive State and Data Abstraction (DD, RG, GD, RH, PK, HP), pp. 455–467.
CAVCAV-1994-GeistB #automation #performance
Efficient Model Checking by Automated Ordering of Transition Relation Partitions (DG, IB), pp. 299–310.
CAVCAV-1994-Hungar #metaprogramming #process
Model Checking of macro Processes (HH), pp. 169–181.
CAVCAV-1994-Manna
Beyond Model Checking (ZM), pp. 220–221.
CAVCAV-1994-McMillan
Hierarchical Representations of Discrete Functions, with Application to Model Checking (KLM), pp. 41–54.
CAVCAV-1994-NaikS #modelling #protocol #using #verification
Modeling and Verification of a Real Life Protocol Using Symbolic Model Checking (VGN, APS), pp. 194–206.
CAVCAV-1994-Peled #on the fly #partial order #reduction
Combining Partial Order Reductions with On-the-fly Model-Checking (DP), pp. 377–390.
CAVCAV-1994-SokolskyS #calculus #incremental #μ-calculus
Incremental Model Checking in the Modal μ-Calculus (OS, SAS), pp. 351–363.
LICSLICS-1994-ZhangSS #calculus #complexity #on the #parallel #μ-calculus
On the Parallel Complexity of Model Checking in the Modal μ-Calculus (SZ, OS, SAS), pp. 154–163.
ICALPICALP-1993-HungarS #process
Local Model Checking for Context-Free Processes (HH, BS), pp. 593–605.
FMFME-1993-Barrett
Model Checking in Practice — The T9000 Virtual Channel Processor (GB), pp. 129–147.
FMFME-1993-WangME #distributed #realtime
Symbolic Model Checking for Distributed Real-Time Systems (FW, AKM, EAE), pp. 632–651.
DACDAC-1993-HojatiSBK #approach
A Unified Approach to Language Containment and Fair CTL Model Checking (RH, TRS, RKB, RPK), pp. 475–481.
TAPSOFTTAPSOFT-1993-Esparza #using
Model Checking Using Net Unfoldings (JE), pp. 613–628.
CAVCAV-1993-ClarkeFJ #logic #symmetry
Exploiting Symmetry In Temporal Logic Model Checking (EMC, TF, SJ), pp. 450–462.
CAVCAV-1993-EmersonJS #calculus #on the #μ-calculus
On Model-Checking for Fragments of μ-Calculus (EAE, CSJ, APS), pp. 385–396.
CAVCAV-1993-EmersonS #symmetry
Symmetry and Model Checking (EAE, APS), pp. 463–478.
CAVCAV-1993-Hungar #parallel #process #proving #theorem proving #verification
Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.
CAVCAV-1993-Peled #using
All from One, One for All: on Model Checking Using Representatives (DP), pp. 409–423.
POPLPOPL-1992-ClarkeGL #abstraction
Model Checking and Abstraction (EMC, OG, DEL), pp. 342–354.
ESOPESOP-1992-Andersen #graph
Model Checking and Boolean Graphs (HRA), pp. 1–19.
CAVCAV-1992-Bradfield #proving
A Proof Assistant for Symbolic Model-Checking (JCB), pp. 316–329.
CAVCAV-1992-CleavelandKS #calculus #performance #μ-calculus
Faster Model Checking for the Modal μ-Calculus (RC, MK, BS), pp. 410–422.
CAVCAV-1992-Kaivola #composition #linear #logic
Compositional Model Checking for Linear-Time Temporal Logic (RK), pp. 248–259.
CAVCAV-1992-RicoBC #realtime
Model-Checking for Real-Time Systems Specified in Lotos (NR, GvB, OC), pp. 288–301.
CAVCAV-1992-ShipleCSB #automation #composition #reduction
Automatic Reduction in CTL Compositional Model Checking (TRS, MC, ALSV, RKB), pp. 234–247.
LICSLICS-1992-HenzingerNSY #realtime
Symbolic Model Checking for Real-time Systems (TAH, XN, JS, SY), pp. 394–406.
ICALPICALP-1991-AlurCD #probability #realtime
Model-Checking for Probabilistic Real-Time Systems (RA, CC, DLD), pp. 115–126.
KRKR-1991-HalpernV #proving #theorem proving
Model Checking vs. Theorem Proving: A Manifesto (JYH, MYV), pp. 325–334.
DACDAC-1991-BurchCL #representation
Representing Circuits More Efficiently in Symbolic Model Checking (JRB, EMC, DEL), pp. 403–407.
CAVCAV-1991-CleavelandS #algorithm #calculus #linear #μ-calculus
A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal μ-Calculus (RC, BS), pp. 48–58.
CAVCAV-1991-EndersFT #generative
Generating BDDs for Symbolic Model Checking in CCS (RE, TF, DT), pp. 203–213.
CAVCAV-1991-Filkorn #functional
Functional Extension of Symbolic Model Checking (TF), pp. 225–232.
CAVCAV-1991-HamaguchiHY #branch #logic #using #verification
Formal Verification of Speed-Dependent Asynchronous Cicuits Using Symbolic Model Checking of branching Time Regular Temporal Logic (KH, HH, SY), pp. 410–420.
CAVCAV-1991-HiraishiHOY #logic #verification
Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification (HH, KH, HO, SY), pp. 214–224.
CAVCAV-1991-ProbstL #partial order
Partial-Order Model Checking: A Guide for the Perplexed (DKP, HFL), pp. 322–331.
CSLCSL-1991-BestE #persistent #petri net
Model Checking of Persistent Petri Nets (EB, JE), pp. 35–52.
LICSLICS-1991-GodefroidW #approach
A Partial Approach to Model Checking (PG, PW), pp. 406–415.
DACDAC-1990-BurchCMD #using #verification
Sequential Circuit Verification Using Symbolic Model Checking (JRB, EMC, KLM, DLD), pp. 46–51.
CAVCAV-1990-CamuratiGPR #using
The Use of Model Checking in ATPG for Sequential Circuits (PC, MG, PP, MSR), pp. 86–95.
CAVCAV-1990-Clarke #explosion #logic #problem
Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem (EMC), p. 1.
CAVCAV-1990-HamaguchiHY #branch #complexity #linear #logic
Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity (KH, HH, SY), pp. 253–262.
CAVCAV-1990-HiraishiMH #logic
Vectorized Model Checking for Computation Tree Logic (HH, SM, KH), pp. 44–53.
LICSLICS-1990-AlurCD #realtime
Model-Checking for Real-Time Systems (RA, CC, DLD), pp. 414–425.
LICSLICS-1990-BurchCMDH
Symbolic Model Checking: 10^20 States and Beyond (JRB, EMC, KLM, DLD, LJH), pp. 428–439.
ICALPICALP-1989-Winskel #calculus
A Note on Model Checking the Modal nu-Calculus (GW), pp. 761–772.
TAPSOFTCAAP-1989-StirlingW #calculus
Local Model Checking in the Modal Mu-Calculus (CS, DW), pp. 369–383.
LICSLICS-1989-ClarkeLM #composition
Compositional Model Checking (EMC, DEL, KLM), pp. 353–362.
ICALPICALP-1987-Josko #liveness
Modelchecking of CTL Formulae under Liveness Assumptions (BJ), pp. 280–289.
LICSLICS-1986-EmersonL #calculus #performance #μ-calculus
Efficient Model Checking in Fragments of the Propositional μ-Calculus (EAE, CLL), pp. 267–278.
POPLPOPL-1985-EmersonL #branch
Modalities for Model Checking: Branching Time Strikes Back (EAE, CLL), pp. 84–96.

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.