BibSLEIGH — model checking tag

model checking

model checking

Tag #model checking

1111 papers:

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