BibSLEIGH — check stem

Used together with:

model (1017)
system (196)
use (190)
base (160)
program (134)

Stem check$ (all stems)

1725 papers:

CBSE-2015-NandiMO #component #contract #probability #realtime #runtime: Stochastic Contracts for Runtime Checking of Component-based Real-time Systems (CN, AM, MO), pp. 111–116.
WICSA-2015-CaraccioloLN #approach #architecture #consistency: A Unified Approach to Architecture Conformance Checking (AC, MFL, ON), pp. 41–50.
DAC-2015-DaiKB #equivalence: Sequential equivalence checking of clock-gated circuits (YYD, KYK, RKB), p. 6.
DAC-2015-MundhenkSLFC #analysis #architecture #model checking #probability #security #using: Security analysis of automotive architectures using probabilistic model checking (PM, SS, ML, SAF, SC), p. 6.
DATE-2015-CaoBFCCAO #feature model #validation: LVS check for photonic integrated circuits: curvilinear feature extraction and validation (RC, JB, JF, LC, JC, AA, IO), pp. 1253–1256.
DATE-2015-ChangD #analysis #model checking #modelling #using: May-happen-in-parallel analysis of ESL models using UPPAAL model checking (CWC, RD), pp. 1567–1570.
DATE-2015-ChenYQFM #evaluation #model checking #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 #model checking #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 #model checking #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.
DATE-2015-SaifhashemiHBB #equivalence #logic #tool support #using: Logical equivalence checking of asynchronous circuits using commercial tools (AS, HHH, PB, PAB), pp. 1563–1566.
DATE-2015-WengCCHW #using: Using structural relations for checking combinationality of cyclic circuits (WCW, YCC, JHC, CYH, CYW), pp. 325–328.
DATE-2015-YanCC #consistency #natural language #specification: Formal consistency checking over specifications in natural languages (RY, CHC, YC), pp. 1677–1682.
FASE-2015-FedyukovichDHS #bound #dependence #detection #model checking: Symbolic Detection of Assertion Dependencies for Bounded Model Checking (GF, ACD, AEJH, NS), pp. 186–201.
TACAS-2015-AbdullaAAJLS #model checking: Stateless Model Checking for TSO and PSO (PAA, SA, MFA, BJ, CL, KFS), pp. 353–367.
TACAS-2015-GiacobbeGGHPP #model checking #network: Model Checking Gene Regulatory Networks (MG, CCG, AG, TAH, TP, TP), pp. 469–483.
TACAS-2015-HansenWCNK #model checking #semantics #statistics: Semantic Importance Sampling for Statistical Model Checking (JPH, LW, SC, DdN, MHK), pp. 241–255.
TACAS-2015-KantLMPBD #independence #model checking #named: LTSmin: High-Performance Language-Independent Model Checking (GK, AL, JM, JvdP, SB, TvD), pp. 692–707.
TACAS-2015-KumarSK #concept #scalability #slicing: Value Slice: A New Slicing Concept for Scalable Property Checking (SK, AS, UPK), pp. 101–115.
TACAS-2015-MolnarDVB #incremental #induction #ltl #model checking #proving: Saturation-Based Incremental LTL Model Checking with Inductive Proofs (VM, DD, AV, TB), pp. 643–657.
TACAS-2015-NutzDMP #contest #memory management #safety: ULTIMATE KOJAK with Memory Safety Checks — (Competition Contribution) (AN, DD, MMM, AP), pp. 458–460.
TACAS-2015-RenaultDKP #automaton #model checking #parallel: Parallel Explicit Model Checking for Generalized Büchi Automata (ER, ADL, FK, DP), pp. 613–627.
TACAS-2015-Thierry-Mieg #model checking #using: Symbolic Model-Checking Using ITS-Tools (YTM), pp. 231–237.
TACAS-2015-Wijs #branch #gpu #similarity: GPU Accelerated Strong and Branching Bisimilarity Checking (AW), pp. 368–383.
SANER-2015-NayrollesHTL #approach #debugging #model checking #named #using: JCHARMING: A bug reproduction approach using crash traces and directed model checking (MN, AHL, ST, AL), pp. 101–110.
SCAM-2015-BanerjeeMS #equivalence #framework #validation: A translation validation framework for symbolic value propagation based equivalence checking of FSMDAs (KB, CAM, DS), pp. 247–252.
SCAM-2015-HuckBU #c++: Checking C++ codes for compatibility with operator overloading (AH, CB, JU), pp. 91–100.
PLDI-2015-Huang #concurrent #model checking #reduction #source code: Stateless model checking concurrent programs with maximal causality reduction (JH), pp. 165–174.
CIAA-2015-Szykula #automaton: Checking Whether an Automaton Is Monotonic Is NP-complete (MS), pp. 279–291.
DLT-2015-FengLQ #word: Path Checking for MTL and TPTL over Data Words (SF, ML, KQ), pp. 326–339.
LATA-2015-Salem #automaton #ltl #model checking #testing: Single-Pass Testing Automata for LTL Model Checking (AEBS), pp. 563–576.
FM-2015-0001K #bound #model checking #using: Property-Driven Fence Insertion Using Reorder Bounded Model Checking (SJ, DK), pp. 291–307.
FM-2015-ChimdyalwarDCVC #abstraction #bound #model checking #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 #model checking: Certificates for Parameterized Model Checking (SC, AM, FZ), pp. 126–142.
FM-2015-KroeningLW #automaton #bound #model checking #proving #safety: Proving Safety with Trace Automata and Bounded Model Checking (DK, ML, GW), pp. 325–341.
FM-2015-Nakajima #behaviour #energy #maude #realtime #using: Using Real-Time Maude to Model Check Energy Consumption Behavior (SN), pp. 378–394.
FM-2015-ZhuYGZZZ #data flow #graph #model checking #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 #model checking #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++ #model checking: Techniques for Memory-Efficient Model Checking of C and C++ Code (PR, VS, JB), pp. 268–282.
ICGT-2015-DyckG #induction #invariant: Inductive Invariant Checking with Partial Negative Application Conditions (JD, HG), pp. 237–253.
DUXU-DD-2015-HertleinHVSW #human-computer #usability #what: Practice What We Preach — Checking the Usability of HCI Conference Websites (FH, BH, MV, TS, CW), pp. 295–305.
HIMI-IKC-2015-HamaguchiMTKN #design #generative #matrix #using: A Method for Generation and Check of Alarm Configurations Using Cause-Effect Matrices for Plant Alarm System Design (TH, BM, KT, NK, MN), pp. 549–556.
MoDELS-2015-PrzigodaHWPD #behaviour #concurrent #modelling #ocl #uml: Checking concurrent behavior in UML/OCL models (NP, CH, RW, JP, RD), pp. 176–185.
ECOOP-2015-Chevalier-Boisvert #effectiveness #lazy evaluation #version control: Simple and Effective Type Check Removal through Lazy Basic Block Versioning (MCB, MF), pp. 101–123.
OOPSLA-2015-DemskyL #model checking #named: SATCheck: SAT-directed stateless model checking for SC and TSO (BD, PL), pp. 20–36.
OOPSLA-2015-ErdwegBKKM #incremental #type checking: A co-contextual formulation of type rules and its application to incremental type checking (SE, OB, EK, MK, MM), pp. 880–897.
OOPSLA-2015-FelgentreffMBH #constraints #programming language #theorem proving: Checks and balances: constraint solving without surprises in object-constraint programming languages (TF, TDM, AB, RH), pp. 767–782.
OOPSLA-2015-JensenMRDV #model checking: Stateless model checking of event-driven applications (CSJ, AM, VR, DD, MTV), pp. 57–73.
PPDP-2015-Miller #logic programming #proving: Proof checking and logic programming (DM), p. 18.
QAPL-2015-BortolussiH #markov #modelling #performance: Efficient Checking of Individual Rewards Properties in Markov Population Models (LB, JH), pp. 32–47.
POPL-2015-BouajjaniEEH #concurrent #refinement: Tractable Refinement Checking for Concurrent Objects (AB, ME, CE, JH), pp. 651–662.
SAC-2015-BouaskerY #anti #constraints #correlation #mining: Key correlation mining by simultaneous monotone and anti-monotone constraints checking (SB, SBY), pp. 851–856.
SAC-2015-CamaraGS0 #adaptation #architecture #game studies #model checking #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 #model checking #verification #web #web service: Model-checking verification of publish-subscribe architectures in web service contexts (GD, MEC, HM, VVR), pp. 1688–1695.
SAC-2015-MilewiczVTQP #c #runtime #source code: Runtime checking C programs (RM, RV, JT, DQ, PP), pp. 2107–2114.
ESEC-FSE-2015-MorenoCGS #adaptation #approach #model checking #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 #model checking #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 #model checking #symbolic computation #testing: Combining Symbolic Execution and Model Checking for Data Flow Testing (TS, ZF, GP, JH, ZS), pp. 654–665.
SPLC-2015-DimovskiABW #model checking #off the shelf #using: Family-based model checking using off-the-shelf model checkers: extended abstract (ASD, ASAS, CB, AW), p. 397.
CGO-2015-HasabnisQS #architecture #code generation #correctness #specification: Checking correctness of code generator architecture specifications (NH, RQ, RS), pp. 167–178.
SOSP-2015-MinKLSK #correctness #debugging #file system #semantics: Cross-checking semantic correctness: the case of finding file system bugs (CM, SK, BL, CS, TK), pp. 361–377.
CADE-2015-Ji #deduction #model checking: CTL Model Checking in Deduction Modulo (KJ), pp. 295–310.
CADE-2015-ZulkoskiGC #algebra #named #satisfiability: MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers (EZ, VG, KC), pp. 607–622.
CAV-2015-DietschHLP #approach #ltl #model checking #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: Model Checking Parameterized Asynchronous Shared-Memory Systems (ADG, JE, PG, RM), pp. 67–84.
CAV-2015-FinkbeinerRS #algorithm #model checking: Algorithms for Model Checking HyperLTL and HyperCTL ^* (BF, MNR, CS), pp. 30–48.
CAV-2015-KonnovVW #abstraction #algorithm #distributed #model checking #smt: SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms (IK, HV, JW), pp. 85–102.
CSL-2015-GrelloisM #higher-order #linear #logic #model checking #relational #semantics: Relational Semantics of Linear Logic and Higher-order Model Checking (CG, PAM), pp. 260–276.
CSL-2015-MolinariMP #logic #model checking: A Model Checking Procedure for Interval Temporal Logics based on Track Representatives (AM, AM, AP), pp. 193–210.
ICLP-J-2015-StulovaMH #runtime: Practical run-time checking via unobtrusive property caching (NS, JFM, MVH), pp. 726–741.
ICST-2015-MidtgaardM #static analysis: QuickChecking Static Analysis Properties (JM, AM), pp. 1–10.
ISSTA-2015-GongPSS #javascript #named: DLint: dynamically checking bad coding practices in JavaScript (LG, MP, MS, KS), pp. 94–105.
LICS-2015-KobayashiL #abstraction #model checking #refinement: Automata-Based Abstraction Refinement for μHORS Model Checking (NK, XL), pp. 713–724.
LICS-2015-Ong #bibliography #higher-order #model checking #perspective: Higher-Order Model Checking: An Overview (LO), pp. 1–15.
SAT-2015-CaiLS #named #satisfiability: CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability (SC, CL, KS), pp. 1–8.
TAP-2015-GogollaHHS #case study #consistency #experience #ocl #uml: Checking UML and OCL Model Consistency: An Experience Report on a Middle-Sized Case Study (MG, LH, FH, MS), pp. 129–136.
VMCAI-2015-GhorbalSP #algebra #difference #proving #set: A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets (KG, AS, AP), pp. 431–448.
CBSE-2014-MateescuSY #model checking #parallel #process #using: Quantifying the parallelism in BPMN processes using model checking (RM, GS, LY), pp. 159–168.
QoSA-2014-OlssonTWE #architecture #consistency #evaluation #game studies: Evaluation of a static architectural conformance checking method in a line of computer games (TO, DT, AW, ME), pp. 113–118.
WICSA-2014-WeinreichB #architecture #automation #consistency: Automatic Reference Architecture Conformance Checking for SOA-Based Software Systems (RW, GB), pp. 95–104.
ASE-2014-PruijtKWB #architecture #named #set: HUSACCT: architecture compliance checking with rich sets of module and rule types (LJP, CK, JMvdW, SB), pp. 851–854.
DAC-2014-MukherjeeAL #approximate: Approximate property checking of mixed-signal circuits (PM, CSA, PL), p. 6.
DAC-2014-ShrivastavaRJW #analysis #control flow #fault: Quantitative Analysis of Control Flow Checking Mechanisms for Soft Errors (AS, AR, RJ, CJW), p. 6.
DATE-2014-HaoRX #behaviour #equivalence #pipes and filters #synthesis: Equivalence checking for function pipelining in behavioral synthesis (KH, SR, FX), pp. 1–6.
DATE-2014-HsuCMGB #architecture #named #performance #validation: ArChiVED: Architectural checking via event digests for high performance validation (CHH, DC, RM, RG, VB), pp. 1–6.
DATE-2014-IannopolloNTS #contract #design #refinement #scalability: Library-based scalable refinement checking for contract-based design (AI, PN, ST, ALSV), pp. 1–6.
VLDB-2014-WuAL0Y #towards: Toward Computational Fact-Checking (YW, PKA, CL, JY, CY), pp. 589–600.
ESOP-2014-ZomerGRS #encapsulation: Checking Linearizability of Encapsulated Extended Operations (OZ, GGG, GR, MS), pp. 311–330.
FASE-2014-BaierDKDKMW #model checking #multi #probability #reasoning #standard: Probabilistic Model Checking and Non-standard Multi-objective Reasoning (CB, CD, SK, MD, JK, SM, SW), pp. 1–16.
FASE-2014-BersaniBGKP #smt: SMT-Based Checking of SOLOIST over Sparse Traces (MMB, DB, CG, SK, PSP), pp. 276–290.
FoSSaCS-2014-Tsukada0 #call-by #complexity #model checking #source code: Complexity of Model-Checking Call-by-Value Programs (TT, NK), pp. 180–194.
TACAS-2014-Ardeshir-LarijaniGN #concurrent #equivalence #protocol #quantum #verification: Verification of Concurrent Quantum Protocols by Equivalence Checking (EAL, SJG, RN), pp. 500–514.
TACAS-2014-SalemDKT #automaton #invariant #model checking #testing #using: Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata (AEBS, ADL, FK, YTM), pp. 440–454.
TACAS-2014-Wang0LWL #automaton #specification: Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata (TW, JS, YL, XW, SL), pp. 310–325.
WRLA-2014-AlrahmanABL #concurrent #maude #memory management #modelling #question #source code: Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude? (YAA, MA, AB, ALL), pp. 21–41.
WRLA-2014-BaeM #infinity #model checking #using: Infinite-State Model Checking of LTLR Formulas Using Narrowing (KB, JM), pp. 113–129.
PLDI-2014-BiswasHSB #named #performance #precise: DoubleChecker: efficient sound and precise atomicity checking (SB, JH, AS, MDB), p. 6.
FLOPS-2014-AmaralFC #named #prolog #testing: PrologCheck — Property-Based Testing in Prolog (CA, MF, VSC), pp. 1–17.
AFL-2014-CarayolH #algorithm #automaton #model checking: Saturation algorithms for model-checking pushdown systems (AC, MH), pp. 1–24.
ICALP-v2-2014-BundalaO #complexity #on the: On the Complexity of Temporal-Logic Path Checking (DB, JO), pp. 86–97.
ICALP-v2-2014-YinFHHT #branch #similarity: Branching Bisimilarity Checking for PRS (QY, YF, CH, MH, XT), pp. 363–374.
LATA-2014-KleinMBK #automaton #model checking #probability #question: Are Good-for-Games Automata Good for Probabilistic Model Checking? (JK, DM, CB, SK), pp. 453–465.
FM-2014-BaiHWLLM #formal method #model checking #named #towards: TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms (GB, JH, JW, YL, ZL, AM), pp. 110–126.
FM-2014-DuggiralaWMVM #modelling #parallel #precedence #protocol: Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol (PSD, LW, SM, MV, CAM), pp. 215–229.
FM-2014-HuPF #bidirectional #programming: Validity Checking of Putback Transformations in Bidirectional Programming (ZH, HP, SF), pp. 1–15.
FM-2014-LakshmiAK #analysis #liveness #reachability #using: Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis (KVL, AA, RK), pp. 335–350.
FM-2014-LinH #composition #concurrent #learning #model checking #synthesis: Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning (SWL, PAH), pp. 416–431.
FM-2014-MarriottC #named: SCJ: Memory-Safety Checking without Annotations (CM, AC), pp. 465–480.
IFM-2014-OliveiraSF #model checking #specification: Model-Checking Circus State-Rich Specifications (MVMO, ACAS, MSCF), pp. 39–54.
SEFM-2014-BianculliGK #logic #metric #pipes and filters #using: Trace Checking of Metric Temporal Logic with Aggregating Modalities Using MapReduce (DB, CG, SK), pp. 144–158.
SEFM-2014-PunSS #behaviour #concurrent: Effect-Polymorphic Behaviour Inference for Deadlock Checking (KIP, MS, VS), pp. 50–64.
SFM-2014-BoerG #monitoring #runtime: Combining Monitoring with Run-Time Assertion Checking (FSdB, SdG), pp. 217–262.
SFM-2014-GmeinerKSVW #algorithm #distributed #fault tolerance #model checking #tutorial: Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms (AG, IK, US, HV, JW), pp. 122–171.
IFL-2014-AmorimGAH #linear #type checking: Really Natural Linear Indexed Type Checking (AAdA, MG, EJGA, JH), p. 5.
ICGT-2014-Delzanno #distributed #model checking #protocol #verification: Parameterized Verification and Model Checking for Distributed Broadcast Protocols (GD), pp. 1–16.
CHI-2014-ArreolaMFCCW #design: From checking on to checking in: designing for low socio-economic status older adults (IA, ZM, MF, KC, KEC, GEW), pp. 1933–1936.
CSCW-2014-KripleanBBKG #on-demand: Integrating on-demand fact-checking with public dialogue (TK, CB, AB, BK, BTG), pp. 1188–1199.
HILT-2014-RathjeR #framework #java #model checking #network #source code: A framework for model checking UDP network programs with Java pathfinder (WR, BR), pp. 81–86.
CIKM-2014-HsiehL #mining: Mining and Planning Time-aware Routes from Check-in Data (HPH, CTL), pp. 481–490.
CIKM-2014-WuL #consistency #evolution #ontology #towards: Towards Consistency Checking over Evolving Ontologies (JW, FL), pp. 909–918.
ICPR-2014-MiyanS #consistency #image #using: Finding Corresponding Patches in Texture Images Using Tensor Consistency Check (SBM, JS), pp. 4021–4026.
KEOD-2014-TongphuS #logic #standard: A Non-standard Instance Checking for the Description Logic ELH (ST, BS), pp. 67–74.
KR-2014-LomuscioM14a #bound #model checking: Model Checking Unbounded Artifact-Centric Systems (AL, JM).
SEKE-2014-ChenX #automation #consistency #mobile #towards #web: Towards Automatic Consistency Checking between Web Application and its Mobile Application (XC, ZX), pp. 53–58.
OOPSLA-2014-BarowyGB #debugging #named #spreadsheet: CheckCell: data debugging for spreadsheets (DWB, DG, EDB), pp. 507–523.
OOPSLA-2014-FeldthausM #correctness #interface #javascript #library #typescript: Checking correctness of TypeScript interfaces for JavaScript libraries (AF, AM), pp. 1–16.
PPDP-2014-Ramsay #abstraction #recursion #safety: Exact Intersection Type Abstractions for Safety Checking of Recursion Schemes (SJR), pp. 175–186.
QAPL-2014-SpielerHZ #markov #model checking #modelling: Model Checking CSL for Markov Population Models (DS, EMH, LZ), pp. 93–107.
POPL-2014-CoughlinC #analysis #composition #invariant: Fissile type analysis: modular checking of almost everywhere invariants (DC, BYEC), pp. 73–86.
POPL-2014-RamsayNO #abstraction #approach #higher-order #model checking #refinement: A type-directed abstraction refinement approach to higher-order model checking (SJR, RPN, CHLO), pp. 61–72.
SAC-2014-MolkaRDCZG #consistency #modelling #process: Conformance checking for BPMN-based process models (TM, DR, MD, AC, XJZ, WG), pp. 1406–1413.
SAC-2014-PereiraS #complexity #deduction #source code: Complexity checking of ARM programs, by deduction (MP, SMdS), pp. 1309–1314.
FSE-2014-Kan #model checking #safety #traceability #verification: Traceability and model checking to support safety requirement verification (SK), pp. 783–786.
ICSE-2014-CaiWC #approach #constraints #dynamic analysis #named #parallel #source code #thread: ConLock: a constraint-based approach to dynamic checking on deadlocks in multithreaded programs (YC, SW, WKC), pp. 491–502.
ICSE-2014-CarzanigaGGMP: Cross-checking oracles from intrinsic software redundancy (AC, AG, AG, AM, MP), pp. 931–942.
ICSE-2014-GorlaTGZ #behaviour: Checking app behavior against app descriptions (AG, IT, FG, AZ), pp. 1025–1035.
ICSE-2014-YangKPR #difference #incremental: Property differencing for incremental checking (GY, SK, SP, NR), pp. 1059–1070.
SLE-2014-BillGKS #model checking #ocl #specification: Model Checking of CTL-Extended OCL Specifications (RB, SG, PK, MS), pp. 221–240.
SPLC-2014-QuintonPBDB #consistency #evolution #feature model #modelling: Consistency checking for the evolution of cardinality-based feature models (CQ, AP, DLB, LD, GB), pp. 122–131.
SPLC-2014-ThumMBHRS #model checking #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.
CGO-2014-NagarakatteMZ #named #pointer: WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking (SN, MMKM, SZ), p. 175.
HPDC-2014-RajachandrasekarPVHWP #architecture #distributed #framework #named: MIC-Check: a distributed check pointing framework for the intel many integrated cores architecture (RR, SP, AV, KH, MWuR, DKP), pp. 121–124.
LCTES-2014-ChaudharyFT #compilation #named #specification: em-SPADE: a compiler extension for checking rules extracted from processor specifications (SC, SF, LT), pp. 105–114.
OSDI-2014-LeesatapornwongsaHJLG #debugging #model checking #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.
CAV-2014-0001A #invariant #random #using: From Invariant Checking to Invariant Inference Using Randomized Search (RS, AA), pp. 88–105.
CAV-2014-ChowdhuryJGD #monitoring #policy #privacy #runtime: Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (OC, LJ, DG, AD), pp. 131–149.
CAV-2014-InversoT0TP #bound #c #concurrent #lazy evaluation #model checking #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 #model checking #recursion #smt #source code: SMT-Based Model Checking for Recursive Programs (AK, AG, SC), pp. 17–34.
ICLP-J-2014-MarpleG #consistency #programming #set: Dynamic Consistency Checking in Goal-Directed Answer Set Programming (KM, GG), pp. 415–427.
ISSTA-2014-LeAGG #haskell #mutation testing #named #source code #testing: MuCheck: an extensible tool for mutation testing of haskell programs (DL, MAA, RG, AG), pp. 429–432.
LICS-CSL-2014-BaierDK #analysis #model checking #probability #trade-off: Trade-off analysis meets probabilistic model checking (CB, CD, SK), p. 10.
LICS-CSL-2014-BojanczykDK #calculus #composition #model checking #theorem #μ-calculus: Decomposition theorems and model-checking for the modal μ-calculus (MB, CD, SK), p. 10.
LICS-CSL-2014-BovaGS #logic #model checking #order #set: Model checking existential logic on partially ordered sets (SB, RG, SS), p. 10.
LICS-CSL-2014-Mahboubi #order #proving #theorem: Computer-checked mathematics: a formal proof of the odd order theorem (AM), p. 1.
LICS-CSL-2014-TsukadaO #composition #game studies #higher-order #model checking: Compositional higher-order model checking via ω-regular games over Böhm trees (TT, CHLO), p. 10.
SAT-2014-HeymanSMLA #using: Dominant Controllability Check Using QBF-Solver and Netlist Optimizer (TH, DS, YM, LL, HAH), pp. 227–242.
SAT-2014-WetzlerHH #named #performance #proving #using: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (NW, MH, WAHJ), pp. 422–429.
TAP-2014-ArcainiGR #abstraction #model checking #testing: An Abstraction Technique for Testing Decomposable Systems by Model Checking (PA, AG, ER), pp. 36–52.
TAP-2014-KosmatovS #analysis #runtime #tutorial: Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses — Tutorial Synopsis (NK, JS), pp. 165–168.
VMCAI-2014-AminofJKR #model checking: Parameterized Model Checking of Token-Passing Systems (BA, SJ, AK, SR), pp. 262–281.
ASE-2013-ArthoHPTWY #communication #distributed #model checking: 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 #model checking #named #source code: BLITZ: Compositional bounded model checking for real-world programs (CYC, VD, DS), pp. 136–146.
ASE-2013-CimattiDT #contract #named #refinement: OCRA: A tool for checking the refinement of temporal contracts (AC, MD, ST), pp. 702–705.
ASE-2013-ZhangCW #concurrent #data type #named #runtime: Round-up: Runtime checking quasi linearizability of concurrent data structures (LZ, AC, CW), pp. 4–14.
DAC-2013-LeiXC #consistency #prototype: Post-silicon conformance checking with virtual prototypes (LL, FX, KC), p. 6.
DAC-2013-WuWLH #algorithm #generative #model checking #satisfiability: A counterexample-guided interpolant generation algorithm for SAT-based model checking (CYW, CAW, CYL, CY(H), p. 6.
DAC-2013-YangRHX #behaviour #design #equivalence #implementation #optimisation #synthesis: Handling design and implementation optimizations in equivalence checking for behavioral synthesis (ZY, SR, KH, FX), p. 6.
DATE-2013-CabodiLV #bound #model checking #optimisation: Optimization techniques for craig interpolant compaction in unbounded model checking (GC, CL, DV), pp. 1417–1422.
DATE-2013-FakihGFR #analysis #architecture #model checking #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-NikolaouSNOI #array #memory management #question: Memory array protection: check on read or check on write? (PN, YS, LN, EÖ, SI), pp. 214–219.
DATE-2013-WelpK #model checking #reachability: QF BV model checking with property directed reachability (TW, AK), pp. 791–796.
ICDAR-2013-PhamDBR #consistency #geometry #locality #performance #robust: Robust Symbol Localization Based on Junction Features and Efficient Geometry Consistency Checking (TAP, MD, SB, JYR), pp. 1083–1087.
PODS-2013-RudolphK #data access #query: Flag & check: data access with monadically defined queries (SR, MK), pp. 151–162.
SIGMOD-2013-GoasdoueKKLMZ #web: Fact checking and analyzing the web (FG, KK, YK, JL, IM, SZ), pp. 997–1000.
ITiCSE-2013-EganM #c #fault #runtime: Reducing novice C programmers’ frustration through improved runtime error checking (MHE, CM), p. 322.
ESOP-2013-BouajjaniDM #robust: Checking and Enforcing Robustness against TSO (AB, ED, RM), pp. 533–553.
ESOP-2013-EneaSS #composition #invariant: Compositional Invariant Checking for Overlaid and Nested Linked Lists (CE, VS, MS), pp. 129–148.
ESOP-2013-KobayashiI #higher-order #model checking #recursion #source code: Model-Checking Higher-Order Programs with Recursive Types (NK, AI), pp. 431–450.
FASE-2013-BeyerL #model checking: Explicit-State Software Model Checking Based on CEGAR and Interpolation (DB, SL), pp. 146–162.
FASE-2013-LasseterC #design pattern #invariant #runtime: Design Pattern-Based Extension of Class Hierarchies to Support Runtime Invariant Checks (JL, JC), pp. 163–178.
FoSSaCS-2013-OrejasBGM #graph transformation #similarity: Checking Bisimilarity for Attributed Graph Transformation (FO, AB, UG, NM), pp. 113–128.
TACAS-2013-Ardeshir-LarijaniGN #equivalence #protocol #quantum: Equivalence Checking of Quantum Protocols (EAL, SJG, RN), pp. 478–492.
TACAS-2013-BenediktLW #ltl #markov #model checking: LTL Model Checking of Interval Markov Chains (MB, RL, JW), pp. 32–46.
TACAS-2013-FalkeMS #bound #c #contest #model checking #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 #model checking #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: Model Checking Database Applications (MG, RM), pp. 549–564.
TACAS-2013-HuangSW #game studies #model checking: Model-Checking Iterated Games (CHH, SS, FW), pp. 154–168.
TACAS-2013-KoleiniRR #data access #model checking #policy: Model Checking Agent Knowledge in Dynamic Access Control Policies (MK, ER, MR), pp. 448–462.
TACAS-2013-MateescuS #model checking #model transformation #named #π-calculus: PIC2LNT: Model Transformation for Model Checking an Applied π-Calculus (RM, GS), pp. 192–198.
TACAS-2013-RenaultDKP #automaton #composition #model checking #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 #model checking: LTL Model-Checking for Malware Detection (FS, TT), pp. 416–431.
TACAS-2013-WijsE #performance: Efficient Property Preservation Checking of Model Refinements (AW, LE), pp. 565–579.
CSMR-2013-JezekHB #analysis #compilation #library: Supplying Compiler’s Static Compatibility Checks by the Analysis of Third-Party Libraries (KJ, LH, PB), pp. 375–378.
ICPC-2013-PruijtKB #analysis #architecture #dependence #on the: On the accuracy of Architecture Compliance Checking support Accuracy of dependency analysis and violation reporting (LP, CK, SB), pp. 172–181.
ICSM-2013-PruijtKB #architecture #case study #comparative #composition #semantics #tool support: Architecture Compliance Checking of Semantically Rich Modular Architectures: A Comparative Study of Tool Support (LP, CK, SB), pp. 220–229.
STOC-2013-CyganKN #performance: Fast hamiltonicity checking via bases of perfect matchings (MC, SK, JN), pp. 301–310.
CIAA-2013-DeganoFM #model checking #towards: Towards Nominal Context-Free Model-Checking (PD, GLF, GM), pp. 109–121.
ICALP-v1-2013-Lampis #bound #graph #model checking: Model Checking Lower Bounds for Simple Graphs (ML), pp. 673–683.
ICALP-v2-2013-Fu #similarity: Checking Equality and Regularity for Normed BPA with Silent Moves (YF), pp. 238–249.
ICALP-v2-2013-GanianHKOST #graph #model checking: FO Model Checking of Interval Graphs (RG, PH, DK, JO, JS, JT), pp. 250–262.
LATA-2013-Ong #automaton #higher-order #model checking #recursion: Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking (LO), pp. 13–41.
LATA-2013-Quaas #automaton #logic #metric #model checking: Model Checking Metric Temporal Logic over Automata with One Counter (KQ), pp. 468–479.
IFM-2013-Larsen #automaton #model checking #statistics: Priced Timed Automata and Statistical Model Checking (KGL), pp. 154–161.
IFM-2013-SongT #api #library #model checking: Model-Checking Software Library API Usage Rules (FS, TT), pp. 192–207.
SEFM-2013-BorekMSR #approach #model checking #modelling: Model Checking of Security-Critical Applications in a Model-Driven Approach (MB, NM, KS, WR), pp. 76–90.
SFM-2013-BortolussiH #approximate #behaviour #markov #modelling: Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation (LB, JH), pp. 113–149.
SFM-2013-BrimCS #biology #model checking: Model Checking of Biological Systems (LB, MC, DS), pp. 63–112.
HCI-AMTE-2013-BratMP #interactive #model checking #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.
HILT-2013-Chaki #bound #model checking: Bounded model checking of high-integrity software (SC), pp. 9–10.
HILT-2013-CourtieuACZRBHG #coq #formal method #runtime #semantics #towards #using: Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq (PC, MVA, TC, ZZ, R, JB, JH, JG, TJ), pp. 21–22.
CAiSE-2013-TaghiabadiFDA #requirements: Diagnostic Information for Compliance Checking of Temporal Compliance Requirements (ERT, DF, BFvD, WMPvdA), pp. 304–320.
EDOC-2013-HeroldMRS #architecture #case study #consistency: Checking Conformance with Reference Architectures: A Case Study (SH, MM, AR, IS), pp. 71–80.
AMT-2013-KuselSWRSK #atl #case study #model transformation #reuse: Reality Check for Model Transformation Reuse: The ATL Transformation Zoo Case Study (AK, JS, MW, WR, WS, GK), pp. 42–51.
ICMT-2013-ButtnerEGL #model transformation #refinement: Checking Model Transformation Refinement (FB, ME, EG, JdL), pp. 158–173.
ICMT-2013-LepperT #performance #validation: Fragmented Validation: A Simple and Efficient Contribution to XSLT Checking (Extended Abstract) (ML, BTyW), pp. 54–55.
MoDELS-2013-ZurowskaD #composition #lazy evaluation #model checking #modelling #uml #using: Model Checking of UML-RT Models Using Lazy Composition (KZ, JD), pp. 304–319.
MoDELS-2013-ZurowskaD #composition #lazy evaluation #model checking #modelling #uml #using: Model Checking of UML-RT Models Using Lazy Composition (KZ, JD), pp. 304–319.
ECOOP-2013-FlanaganF #detection #named: RedCard: Redundant Check Elimination for Dynamic Race Detectors (CF, SNF), pp. 255–280.
ECOOP-2013-ThomsenCADE #invariant: Reducing Lookups for Invariant Checking (JGT, CC, KJA, JD, EE), pp. 426–450.
OOPSLA-2013-NorrisD #c #c++ #concurrent #data type #named: CDSchecker: checking concurrent data structures written with C/C++ atomics (BN, BD), pp. 131–150.
OOPSLA-2013-SharmaSCA #data-driven #equivalence: Data-driven equivalence checking (RS, ES, BRC, AA), pp. 391–406.
GPCE-2013-KolesnikovRHA #comparison #type checking: A comparison of product-based, feature-based, and family-based type checking (SSK, AvR, CH, SA), pp. 115–124.
LOPSTR-2013-Seki #logic programming #model checking #source code: Extending Co-logic Programs for Branching-Time Model Checking (HS), pp. 127–144.
POPL-2013-BonchiP #automaton #bisimulation #congruence #equivalence #nondeterminism: Checking NFA equivalence with bisimulations up to congruence (FB, DP), pp. 457–468.
SAC-2013-AnconaBM #consistency #dynamic analysis #multi #protocol: Constrained global types for dynamic checking of protocol conformance in multi-agent systems (DA, MB, VM), pp. 1377–1379.
SAC-2013-GouwBJW #case study #industrial #java #runtime #source code: Run-time checking of data- and protocol-oriented properties of Java programs: an industrial case study (SdG, FSdB, EBJ, PYHW), pp. 1573–1578.
ESEC-FSE-2013-AroraSBZG #automation #consistency #flexibility #named: RUBRIC: a flexible tool for automated checking of conformance to requirement boilerplates (CA, MS, LCB, FZ, RG), pp. 599–602.
ESEC-FSE-2013-LahiriMSH #difference: Differential assertion checking (SKL, KLM, RS, CH), pp. 345–355.
ESEC-FSE-2013-SongT #automaton #detection #model checking #named: PoMMaDe: pushdown model-checking for malware detection (FS, TT), pp. 607–610.
ESEC-FSE-2013-ZervoudakisREF #model checking #verification: Cascading verification: an integrated method for domain-specific model checking (FZ, DSR, SGE, AF), pp. 400–410.
ICSE-2013-CordySHL #model checking #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-TianD #detection #model checking: Detecting spurious counterexamples efficiently in abstract model checking (CT, ZD), pp. 202–211.
CAV-2013-AlglaveKT #bound #concurrent #model checking #partial order #performance: Partial Orders for Efficient Bounded Model Checking of Concurrent Software (JA, DK, MT), pp. 141–157.
CAV-2013-BinghamBEG #concurrent #distributed #model checking: Distributed Explicit State Model Checking of Deadlock Freedom (BDB, JDB, JE, MRG), pp. 235–241.
CAV-2013-BrimCDS #model checking #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 #model checking #probability #synthesis: Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis (KC, AG, JK), pp. 559–575.
CAV-2013-ChevalCP #how #privacy: Lengths May Break Privacy — Or How to Check for Equivalences with Length (VC, VC, AP), pp. 708–723.
CAV-2013-ClaessenFIPW #model checking #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 #model checking #towards #using: Towards Distributed Software Model-Checking Using Decision Diagrams (MC, SB, FK, YTM), pp. 830–845.
CAV-2013-HeizmannHP #automaton #model checking #people: Software Model Checking for People Who Love Automata (MH, JH, AP), pp. 36–52.
CAV-2013-JegourelLS #model checking #statistics: Importance Splitting for Statistical Model Checking Rare Properties (CJ, AL, SS), pp. 576–591.
CAV-2013-KomuravelliGCC #abstraction #automation #bound #model checking #smt: Automatic Abstraction in SMT-Based Unbounded Software Model Checking (AK, AG, SC, EMC), pp. 846–862.
CAV-2013-LaarmanODLP #abstraction #automaton #manycore #using: Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction (AL, MCO, AED, KGL, JvdP), pp. 968–983.
CAV-2013-ManciniMMMMT #model checking #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 #model checking: Abstraction Based Model-Checking of Stability of Hybrid Systems (PP, MGS), pp. 280–295.
CAV-2013-StewartEY #automaton #bound #model checking #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 #model checking #recursion: Saturation-Based Model Checking of Higher-Order Recursion Schemes (CHB, NK), pp. 129–148.
CSL-2013-Goller #concurrent #model checking #parametricity: The Fixed-Parameter Tractability of Model Checking Concurrent Systems (SG), pp. 332–347.
ICLP-J-2013-GrecoMT #bottom-up #evaluation #logic programming #termination: Logic programming with function symbols: Checking termination of bottom-up evaluation through program adornments (SG, CM, IT), pp. 737–752.
ICST-2013-LinD #concurrent #java: CHECK-THEN-ACT Misuse of Java Concurrent Collections (YL, DD), pp. 164–173.
ICST-2013-YeolekarUAKV #generative #model checking #scalability #testing #using: Scaling Model Checking for Test Generation Using Dynamic Inference (AY, DU, VA, SK, RV), pp. 184–191.
ISSTA-2013-GuiSLSDW #model checking #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.
ISSTA-2013-YiQTR #contract: Expressing and checking intended changes via software change contracts (JY, DQ, SHT, AR), pp. 1–11.
LICS-2013-BolligKM #complexity #model checking #multi: The Complexity of Model Checking Multi-stack Systems (BB, DK, RM), pp. 163–172.
LICS-2013-BoralS #model checking #parse tree: Model-Checking Parse Trees (AB, SS), pp. 153–162.
LICS-2013-EickmeyerKK #first-order #graph #invariant #logic #model checking: Model Checking for Successor-Invariant First-Order Logic on Minor-Closed Graph Classes (KE, KiK, SK), pp. 134–142.
RTA-2013-BaeEM #infinity #logic #model checking #using: Abstract Logical Model Checking of Infinite-State Systems Using Narrowing (KB, SE, JM), pp. 81–96.
TAP-2013-AichernigJK #generative #incremental #refinement #testing: Incremental Refinement Checking for Test Case Generation (BKA, EJ, MK), pp. 1–19.
TLCA-2013-FridlenderP #algorithm #evaluation #normalisation #type system: A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation (DF, MP), pp. 140–155.
TLCA-2013-SalvatiW #modelling #recursion #using: Using Models to Model-Check Recursive Schemes (SS, IW), pp. 189–204.
VMCAI-2013-Leitner-FischerL #modelling: Causality Checking for Complex System Models (FLF, SL), pp. 248–267.
CBSE-2012-BenesBCO #analysis #component #development #model checking #probability #reliability: Reliability analysis in component-based development via probabilistic model checking (NB, BB, IC, RO), pp. 83–92.
DAC-2012-ChatterjeeKMZB #architecture: Checking architectural outputs instruction-by-instruction on acceleration platforms (DC, AK, RM, AZ, VB), pp. 955–961.
DAC-2012-ChouHHH #design #model checking: Symbolic model checking on SystemC designs (CNC, YSH, CH, CY(H), pp. 327–333.
DAC-2012-HaoRX #behaviour #equivalence #pipes and filters: Equivalence checking for behaviorally synthesized pipelines (KH, SR, FX), pp. 344–349.
DATE-2012-TheelenKW #data flow #model checking: Model checking of Scenario-Aware Dataflow with CADP (BDT, JPK, HW), pp. 653–658.
ITiCSE-2012-Johnson #automation #consistency #generative #interface #named #testing: SpecCheck: automated generation of tests for interface conformance (CJ), pp. 186–191.
ESOP-2012-Lochbihler #formal method #java #memory management: Java and the Java Memory Model — A Unified, Machine-Checked Formalisation (AL), pp. 497–517.
FASE-2012-Aalst #consistency #distributed #process: Distributed Process Discovery and Conformance Checking (WMPvdA), pp. 1–25.
FoSSaCS-2012-BolligCGK #model checking #word: Model Checking Languages of Data Words (BB, AC, PG, KNK), pp. 391–405.
FoSSaCS-2012-GollerHOW #automaton #model checking #parametricity: Branching-Time Model Checking of Parametric One-Counter Automata (SG, CH, JO, JW), pp. 406–420.
FoSSaCS-2012-Kartzow #automaton #exponential #first-order #model checking: First-Order Model Checking on Nested Pushdown Trees is Complete for Doubly Exponential Alternating Time (AK), pp. 376–390.
TACAS-2012-BarbotHP #model checking #statistics: Coupling and Importance Sampling for Statistical Model Checking (BB, SH, CP), pp. 331–346.
TACAS-2012-CairesV #concurrent #logic #model checking #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 #model checking: Context-Bounded Model Checking with ESBMC 1.17 — (Competition Contribution) (LCC, JM, DN, BF), pp. 534–537.
TACAS-2012-HolzlN #model checking #verification: Verifying pCTL Model Checking (JH, TN), pp. 347–361.
TACAS-2012-JegourelLS #framework #model checking #performance #statistics: A Platform for High Performance Statistical Model Checking — PLASMA (CJ, AL, SS), pp. 498–503.
TACAS-2012-JinYS #java #memory management #model checking: Java Memory Model-Aware Model Checking (HJ, TYK, BAS), pp. 220–236.
TACAS-2012-LangM #equation #lts #model checking #network #using: Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems (FL, RM), pp. 141–156.
TACAS-2012-SongT #automaton #detection #model checking: Pushdown Model Checking for Malware Detection (FS, TT), pp. 110–125.
WRLA-2012-BaeM #locality #model checking: Model Checking LTLR Formulas under Localized Fairness (KB, JM), pp. 99–117.
WRLA-2012-LepriAO #maude #model checking #realtime: Timed CTL Model Checking in Real-Time Maude (DL, EÁ, PCÖ), pp. 182–200.
CSMR-2012-LytraTZ #architecture #component #consistency #constraints #design #evolution #modelling: Constraint-Based Consistency Checking between Design Decisions and Component Models for Supporting Software Architecture Evolution (IL, HT, UZ), pp. 287–296.
MSR-2012-PosnettDF #correlation: MIC check: A correlation tactic for ESE data (DP, PTD, VF), pp. 22–31.
PEPM-2012-Xu #contract #hybrid: Hybrid contract checking via symbolic simplification (DNX), pp. 107–116.
FLOPS-2012-TobitaTK #analysis #higher-order #model checking: Exact Flow Analysis by Higher-Order Model Checking (YT, TT, NK), pp. 275–289.
DLT-2012-ChenL #regular expression: Checking Determinism of Regular Expressions with Counting (HC, PL), pp. 332–343.
LATA-2012-TangO #automaton #model checking #on the: On Model Checking for Visibly Pushdown Automata (NVT, HO), pp. 408–419.
FM-2012-GrumbergMY #behaviour #model checking #modelling #uml: Applying Software Model Checking Techniques for Behavioral UML Models (OG, YM, KY), pp. 277–292.
FM-2012-SongT #detection #model checking #performance #using: Efficient Malware Detection Using Model-Checking (FS, TT), pp. 418–433.
IFM-2012-RochaBCN #bound #comprehension #debugging #model checking #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 #model checking #revisited #static analysis: Model Checking as Static Analysis: Revisited (FZ, FN, HRN), pp. 99–112.
SEFM-2012-AbdelhalimST #approach #effectiveness #model checking #optimisation: An Optimization Approach for Effective Formalized fUML Model Checking (IA, SS, HT), pp. 248–262.
SEFM-2012-BarnatBB #requirements: Checking Sanity of Software Requirements (JB, PB, LB), pp. 48–62.
ICFP-2012-NeatherwayRO #algorithm #higher-order #model checking: A traversal-based algorithm for higher-order model checking (RPN, SJR, CHLO), pp. 353–364.
IFL-2012-ReichNR #lazy evaluation #roadmap: Advances in Lazy SmallCheck (JSR, MN, CR), pp. 53–70.
GT-VMT-2012-Heussner #communication #graph #graph grammar #model checking #process: Model Checking Communicating Processes: Run Graphs, Graph Grammars, and MSO (AH).
ICGT-2012-BlumeBEK #automaton #graph #implementation #invariant #performance: Efficient Symbolic Implementation of Graph Automata with Applications to Invariant Checking (CB, HJSB, DE, BK), pp. 264–278.
ICGT-2012-GieseL #automation #behaviour #invariant #model transformation #towards #verification: Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking (HG, LL), pp. 249–263.
CHI-2012-BirnholtzBF #behaviour: Do you see that I see?: effects of perceived visibility on awareness checking behavior (JPB, NB, SRF), pp. 1765–1774.
CHI-2012-DunlopL #multi #optimisation: Multidimensional pareto optimization of touchscreen keyboards for speed, familiarity and improved spell checking (MDD, JL), pp. 2669–2678.
AdaEurope-2012-FariaMP #ada #approach #model checking #source code: An Approach to Model Checking Ada Programs (JMF, JM, JSP), pp. 105–118.
HILT-2012-BeltCHR #ada #automation #contract #using #verification: Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan (JB, PC, JH, R), pp. 3–4.
HILT-2012-EilersK #adaptation #runtime: Adapting ACATS for use with run-time checks suppressed (DE, TK), pp. 97–102.
HILT-2012-SchonbergP #ada #implementation: Implementation of a simple dimensionality checking system in Ada 2012 (ES, VP), pp. 35–42.
ICEIS-v2-2012-AokiOOM #model checking #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 #model checking #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.
CIKM-2012-BonchiFNSV #interactive: Interactive and context-aware tag spell check and correction (FB, OF, FMN, FS, HV), pp. 1869–1873.
CIKM-2012-GaoTL #correlation #modelling #named #network #social: gSCorr: modeling geo-social correlations for new check-ins on location-based social networks (HG, JT, HL), pp. 1582–1586.
KR-2012-GiordanoMD #bound #model checking: Achieving Completeness in Bounded Model Checking of Action Theories in ASP (LG, AM, DTD).
RecSys-2012-SklarSH #realtime #recommendation: Recommending interesting events in real-time with foursquare check-ins (MS, BS, AH), pp. 311–312.
SEKE-2012-SalamahEO #automaton #consistency #ltl #using: Consistency Checks of System Properties Using LTL and Büchi Automata (SS, ME, OO), pp. 39–44.
MoDELS-2012-RederE #consistency #design #incremental: Incremental Consistency Checking for Complex Design Rules and Larger Model Changes (AR, AE), pp. 202–218.
MoDELS-2012-VierhauserGHHL #consistency #framework #industrial #modelling #product line: Applying a Consistency Checking Framework for Heterogeneous Models and Artifacts in Industrial Product Lines (MV, PG, WH, GH, DL), pp. 531–545.
MoDELS-2012-RederE #consistency #design #incremental: Incremental Consistency Checking for Complex Design Rules and Larger Model Changes (AR, AE), pp. 202–218.
MoDELS-2012-VierhauserGHHL #consistency #framework #industrial #modelling #product line: Applying a Consistency Checking Framework for Heterogeneous Models and Artifacts in Industrial Product Lines (MV, PG, WH, GH, DL), pp. 531–545.
ECOOP-2012-HuangDME: Inference and Checking of Object Ownership (WH, WD, AM, MDE), pp. 181–206.
OOPSLA-2012-HuangMDE: Reim & ReImInfer: checking and inference of reference immutability and method purity (WH, AM, WD, MDE), pp. 879–896.
OOPSLA-2012-RosuS #logic #reachability #using: Checking reachability using matching logic (GR, AS), pp. 555–574.
TOOLS-EUROPE-2012-CatanoHR #formal method #named #network #policy #privacy #social: Poporo: A Formal Methods Tool for Fast-Checking of Social Network Privacy Policies (NC, SH, CR), pp. 9–16.
LOPSTR-2012-AngelisFPP #model checking: Specialization with Constrained Generalization for Software Model Checking (EDA, FF, AP, MP), pp. 51–70.
QAPL-2012-BulychevDLMPLW #automaton #model checking #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 #model checking #probability: Measuring Progress of Probabilistic LTL Model Checking (ECB, FvB), pp. 33–47.
QAPL-2012-Giro #model checking #performance: Efficient computation of exact solutions for quantitative model checking (SG), pp. 17–32.
POPL-2012-StampoulisS #proving: Static and user-extensible proof checking (AS, ZS), pp. 273–284.
RE-2012-GreenyerSCH #consistency #performance #product line #specification: Efficient consistency checking of scenario-based product-line specifications (JG, AMS, MC, PH), pp. 161–170.
SAC-2012-AccorsiS #consistency #mining #on the #process #security: On the exploitation of process mining for security audits: the conformance checking case (RA, TS), pp. 1709–1716.
SAC-2012-DamianiPW #object-oriented #programming #type system: A type system for checking specialization of packages in object-oriented programming (FD, APH, YW), pp. 1737–1742.
SAC-2012-KeshishzadehIM #automaton #framework #model checking: A Büchi automata based model checking framework for reo connectors (SK, MI, AM), pp. 1536–1543.
SAC-2012-PoizatS: Checking the realizability of BPMN 2.0 choreographies (PP, GS), pp. 1927–1934.
FSE-2012-BeyerHKW #model checking #verification: Conditional model checking: a technique to pass information between verifiers (DB, TAH, MEK, PW), p. 57.
FSE-2012-MilanovaH: Inference and checking of context-sensitive pluggable types (AM, WH), p. 26.
ICSE-2012-CordyCPSHL #abstraction #model checking #product line: Simulation-based abstractions for software product-line model checking (MC, AC, GP, PYS, PH, AL), pp. 672–682.
ICSE-2012-PradelJAG #api #consistency #multi #protocol #specification: Statically checking API protocol conformance with mined multi-object specifications (MP, CJ, JA, TRG), pp. 925–935.
ICSE-2012-SongHLSLD #approach #model checking #multi #probability: Analyzing multi-agent systems with probabilistic model checking approach (SS, JH, YL, JS, HfL, JSD), pp. 1337–1340.
ICSE-2012-SongT #invariant #metadata: Metadata invariants: Checking and inferring metadata coding conventions (MS, ET), pp. 694–704.
CGO-2012-HasabnisMS #bound: Light-weight bounds checking (NH, AM, RS), pp. 135–144.
LCTES-2012-YuYWCC #consistency #parallel #source code: Symbolic consistency checking of OpenMp parallel programs (FY, SCY, FW, GCC, CCC), pp. 139–148.
CAV-2012-CimattiG #model checking: Software Model Checking via IC3 (AC, AG), pp. 277–293.
CAV-2012-Dill #biology #model checking: Model Checking Cell Biology (DLD), p. 2.
CAV-2012-HassanBS #incremental #induction #model checking: Incremental, Inductive CTL Model Checking (ZH, ARB, FS), pp. 532–547.
CAV-2012-JegourelLS #model checking #optimisation #parametricity #statistics: Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking (CJ, AL, SS), pp. 327–342.
CAV-2012-RolliniSS #model checking: Leveraging Interpolant Strength in Model Checking (SFR, OS, NS), pp. 193–209.
ICLP-2012-Angelis #model checking: Software Model Checking by Program Specialization (EDA), pp. 439–444.
ICLP-J-2012-GorlinRS #logic programming #model checking #probability: Model checking with probabilistic tabled logic programming (AG, CRR, SAS), pp. 681–700.
ICST-2012-ChoudharyPO #crawling #detection #difference #named #web: CrossCheck: Combining Crawling and Differencing to Better Detect Cross-browser Incompatibilities in Web Applications (SRC, MRP, AO), pp. 171–180.
ICST-2012-GligoricMM #model checking #named #programming language: X10X: Model Checking a New Programming Language with an “Old” Model Checker (MG, PCM, DM), pp. 11–20.
ICST-2012-PetrenkoSY #finite #generative #nondeterminism #sequence #state machine: Generating Checking Sequences for Nondeterministic Finite State Machines (AP, AdSS, NY), pp. 310–319.
IJCAR-2012-EmmerKKSV #bound #model checking #word: EPR-Based Bounded Model Checking at Word Level (ME, ZK, KK, CS, AV), pp. 210–224.
LICS-2012-BundalaOW #bound #model checking #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 #model checking #monad: First-Order and Monadic Second-Order Model-Checking on Ordered Structures (VE, SK, SS), pp. 275–284.
TAP-2012-ArmandoPCMB #automation #model checking #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 #model checking #symbolic computation #testing: Combining Model Checking and Symbolic Execution for Software Testing (CSP), p. 2.
VMCAI-2012-Bugaychenko #diagrams #model checking #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: Model Checking Information Flow in Reactive Systems (RD, BF, MK, MNR, HS), pp. 169–185.
ECSA-2011-AdersbergerP #architecture #consistency #named #traceability #uml: ReflexML: UML-Based Architecture-to-Code Traceability and Consistency Checking (JA, MP), pp. 344–359.
ASE-2011-Halfond #web: Domain and value checking of web application invocation arguments (WGJH), pp. 544–547.
ASE-2011-LeungwattanakitAHTY #distributed #model checking #process: Model checking distributed systems by combining caching and process checkpointing (WL, CA, MH, YT, MY), pp. 103–112.
ASE-2011-Li #consistency #natural language #requirements #towards: Toward consistency checking of natural language temporal requirements (WL), pp. 651–655.
ASE-2011-MehlitzTU #model checking #named #user interface: JPF-AWT: Model checking GUI applications (PCM, OT, MU), pp. 584–587.
ASE-2011-NguyenSLD #framework #model checking: A model checking framework for hierarchical systems (TKN, JS, YL, JSD), pp. 633–636.
ASE-2011-OverbeyJ #analysis #difference #lightweight #refactoring #reuse #tool support: Differential precondition checking: A lightweight, reusable analysis for refactoring tools (JLO, REJ), pp. 303–312.
ASE-2011-VakiliD #declarative #model checking #modelling #using: Using model checking to analyze static properties of declarative models (AV, NAD), pp. 428–431.
DAC-2011-MukherjeeFBL #automation #linear #scalability: Automatic stability checking for large linear analog integrated circuits (PM, GPF, RB, PL), pp. 304–309.
DAC-2011-NguyenWSK #abstraction #hardware: Formal hardware/software co-verification by interval property checking with abstraction (MDN, MW, DS, WK), pp. 510–515.
DATE-2011-CabodiN #model checking #multi: Optimized model checking of multiple properties (GC, SN), pp. 543–546.
DATE-2011-MiyaseWAFYK #generative #testing: Transition-Time-Relation based capture-safety checking for at-speed scan test generation (KM, XW, MA, HF, YY, SK), pp. 895–898.
DATE-2011-YehHWL #framework #simulation: Speeding Up MPSoC virtual platform simulation by Ultra Synchronization Checking Method (YFY, CYH, CAW, HCL), pp. 353–358.
ICDAR-2011-LiuC #image: Binarizing the Courtesy Amount Field on Color Chinese Bank Check Images (DL, YC), pp. 774–778.
ICDAR-2011-SadriAJFH #recognition: A New System for Recognition of Handwritten Persian Bank Checks (JS, YA, MJJ, AF, MH), pp. 925–930.
VLDB-2011-GrecoST #termination: Stratification Criteria and Rewriting Techniques for Checking Chase Termination (SG, FS, IT), pp. 1158–1168.
ITiCSE-2011-StrieweG #automation #diagrams #uml: Automated checks on UML diagrams (MS, MG), pp. 38–42.
FASE-2011-ErmelGLT #behaviour #consistency #control flow #functional #modelling: Modeling with Plausibility Checking: Inspecting Favorable and Critical Signs for Consistency between Control Flow and Functional Behavior (CE, JG, LL, GT), pp. 156–170.
FASE-2011-LiXBL #automaton #model checking: Model Checking Büchi Pushdown Systems (JL, FX, TB, VL), pp. 141–155.
FASE-2011-OudinetDGLP #model checking #monte carlo: Uniform Monte-Carlo Model Checking (JO, AD, MCG, RL, SP), pp. 127–140.
FoSSaCS-2011-Kobayashi #algorithm #automaton #higher-order #linear #model checking #recursion: A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes (NK0), pp. 260–274.
TACAS-2011-BarbotCHKM #linear #model checking #performance #realtime: Efficient CTMC Model Checking of Linear Real-Time Objectives (BB, TC, TH, JPK, AM), pp. 128–142.
TACAS-2011-TalupurH #model checking #using: Biased Model Checking Using Flows (MT, HH), pp. 239–253.
ICPC-2011-CordyR #named #open source #performance #source code: DebCheck: Efficient Checking for Open Source Code Clones in Software Systems (JRC, CKR), pp. 217–218.
ICSM-2011-BrunetGF #consistency #design #evaluation #testing #usability: Structural conformance checking with design tests: An evaluation of usability and calability (JB, DSG, JCAdF), pp. 143–152.
ICSM-2011-RupakhetiH #implementation #java #named #similarity: EQ: Checking the implementation of equality in Java (CRR, DH), pp. 590–593.
SCAM-2011-Mehlich #c #memory management #named #validation: CheckPointer — A C Memory Access Validator (MM), pp. 165–172.
PLDI-2011-BurnimENS #correctness #named #nondeterminism #parallel #runtime #specification: NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness (JB, TE, GCN, KS), pp. 401–414.
PLDI-2011-KobayashiSU #abstraction #higher-order #model checking: Predicate abstraction and CEGAR for higher-order model checking (NK, RS, HU), pp. 222–233.
SAS-2011-MonniauxG #bound #fixpoint #model checking #using: Using Bounded Model Checking to Focus Fixpoint Iterations (DM, LG), pp. 369–385.
AFL-2011-CanoJ: Varieties of Languages and Frontier Check (AC, EJ), pp. 153–167.
ICALP-v2-2011-FischerK #calculus #hybrid #linear #model checking #μ-calculus: Model Checking the Quantitative μ-Calculus on Linear Hybrid Systems (DF, LK), pp. 404–415.
ICALP-v2-2011-ZhangJNH #model checking: Automata-Based CSL Model Checking (LZ, DNJ, FN, HH), pp. 271–282.
FM-2011-RozierV #approach #encoding #ltl #multi #satisfiability: A Multi-encoding Approach for LTL Symbolic Satisfiability Checking (KYR, MYV), pp. 417–431.
SEFM-2011-CrespoK #framework #logic #relational: A Machine-Checked Framework for Relational Separation Logic (JMC, CK), pp. 122–137.
SEFM-2011-MorseCNF #bound #ltl #model checking: Context-Bounded Model Checking of LTL Properties for ANSI-C Software (JM, LCC, DN, BF), pp. 302–317.
SEFM-2011-VassevH #case study #experience #model checking: Developing Model-Checking Mechanisms for ASSL: An Experience Report (EV, MH), pp. 19–34.
ICFP-2011-GillF #fault #implementation #performance: Deriving an efficient FPGA implementation of a low density parity check forward error corrector (AG, AF), pp. 209–220.
GT-VMT-2011-VandinL #graph #maude #model checking #towards: Towards a Maude Tool for Model Checking Temporal Graph Properties (AV, ALL).
HIMI-v2-2011-SwierengaADP #design: Real-World User-Centered Design: The Michigan Workforce Background Check System (SJS, FA, TAD, LAP), pp. 325–334.
SIGAda-2011-BeltHRCHD #contract #execution #symbolic computation #using: Enhancing spark’s contract checking facilities using symbolic execution (JB, JH, R, PC, DH, XD), pp. 47–60.
SIGAda-2011-Rosen #ada #design #standard: Designing and checking coding standards for ada (JPR), pp. 13–14.
EDOC-2011-AdriansyahDA #consistency #cost analysis #using: Conformance Checking Using Cost-Based Fitness Analysis (AA, BFvD, WMPvdA), pp. 55–64.
ICEIS-J-2011-PereiraBOM #consistency #process #set: A Set of Well-Formedness Rules to Checking the Consistency of the Software Processes Based on SPEM 2.0 (EBP, RMB, TCO, MCM), pp. 284–299.
KDIR-2011-DeruyverH #approach #consistency #graph #image #information management #semantics: Semantic Graphs and Arc Consistency Checking — The Renewal of an Old Approach for Information Extraction from Images (AD, YH), pp. 515–522.
SEKE-2011-ChenF #aspectj #model checking: Model Checking Framework-based Applications with AspectJ Assistance (ZC, SF), pp. 296–301.
SEKE-2011-GeigerSW #automation #consistency #towards: Towards Automated Conformance Checking of ebBP-ST Choreographies and Corresponding WS-BPEL Based Orchestrations (MG, AS, GW), pp. 566–571.
SEKE-2011-LemosSLO #consistency #development #mining #process: Conformance Checking of Software Development Processes Through Process Mining (AML, CCS, RMFL, CALO), pp. 654–659.
MoDELS-2011-MoffettBD #consistency #model checking #protocol #uml #using #verification: Verifying UML-RT Protocol Conformance Using Model Checking (YM, AB, JD), pp. 410–424.
MoDELS-2011-MoffettBD #consistency #model checking #protocol #uml #using #verification: Verifying UML-RT Protocol Conformance Using Model Checking (YM, AB, JD), pp. 410–424.
OOPSLA-2011-AllenHKLRCS #composition #inheritance #morphism #multi #parametricity #polymorphism #type checking: Type checking modular multiple dispatch with parametric polymorphism and multiple inheritance (EEA, JH, SK, VL, SR, DC, GLSJ), pp. 973–992.
OOPSLA-2011-LiT #exception #interface #java #named: JET: exception checking in the Java native interface (SL, GT), pp. 345–358.
OOPSLA-2011-SonMS #named #security #what: RoleCast: finding missing security checks when you do not know what checks are (SS, KSM, VS), pp. 1069–1084.
PPDP-2011-SchernhammerM #axiom #incremental #recursion #specification: Incremental checking of well-founded recursive specifications modulo axioms (FS, JM), pp. 5–16.
PADL-2011-Christiansen #named #strict: Sloth — A Tool for Checking Minimal-Strictness (JC), pp. 160–174.
PADL-2011-MeraTLH #debugging #logic programming #performance #profiling #runtime #source code: Profiling for Run-Time Checking of Computational Properties and Performance Debugging in Logic Programs (EM, TT, PLG, MVH), pp. 38–53.
SAC-2011-KangR #automation #named #testing: FortressCheck: automatic testing for generic properties (SK, SR), pp. 1290–1296.
ESEC-FSE-2011-CifuentesKLHVBZCTH #fault #scalability #using: Static deep error checking in large system applications using parfait (CC, NK, LL, NH, MV, AB, JZ, AC, DT, CH), pp. 432–435.
ESEC-FSE-2011-DemuthLE #consistency #flexibility #modelling #multi: Cross-layer modeler: a tool for flexible multilevel modeling with consistency checking (AD, RELH, AE), pp. 452–455.
ESEC-FSE-2011-DriscollBR #consistency: Checking conformance of a producer and a consumer (ED, AB, TWR), pp. 113–123.
ICSE-2011-AraujoBL #concurrent #contract #java #modelling #runtime: Enabling the runtime assertion checking of concurrent contracts for the Java modeling language (WA, LCB, YL), pp. 786–795.
ICSE-2011-ClassenHSL #model checking #product line: Symbolic model checking of software product lines (AC, PH, PYS, AL), pp. 321–330.
ICSE-2011-CordeiroF #bound #concurrent #model checking #multi #smt #thread #using #verification: Verifying multi-threaded software using smt-based context-bounded model checking (LC, BF), pp. 331–340.
ICSE-2011-FilieriGT #model checking #performance #probability #runtime: Run-time efficient probabilistic model checking (AF, CG, GT), pp. 341–350.
ICSE-2011-Zhang11a #automation #scalability: Scalable automatic linearizability checking (SJZ), pp. 1185–1187.
LDTA-2011-SergeyC #automaton #recursion #type checking: From type checking by recursive descent to type checking with an abstract machine (IS, DC), p. 2.
SPLC-2011-GhezziS #approach #model checking #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.
ASPLOS-2011-BurnimNS #parallel #semantics #source code #specification #thread: Specifying and checking semantic atomicity for multithreaded programs (JB, GCN, KS), pp. 79–90.
CC-2011-JoynerBS #analysis #array #bound: Subregion Analysis and Bounds Check Elimination for High Level Arrays (MJ, ZB, VS), pp. 246–265.
CGO-2011-BrueningZ #memory management: Practical memory checking with Dr. Memory (DB, QZ), pp. 213–223.
HPCA-2011-AndersonFCE #architecture #javascript #mobile: Checked Load: Architectural support for JavaScript type-checking on mobile processors (OA, EF, LC, SJE), pp. 419–430.
SOSP-2011-GuoWZHYZ #interface #model checking #reduction: Practical software model checking via dynamic interface reduction (HG, MW, LZ, GH, JY, LZ), pp. 265–278.
CAV-2011-BaeM #ltl #model checking #parametricity: State/Event-Based LTL Model Checking under Parametric Generalized Fairness (KB, JM), pp. 132–148.
CAV-2011-BuchholzHHZ #algorithm #model checking: Model Checking Algorithms for CTMDPs (PB, EMH, HH, LZ), pp. 225–242.
CAV-2011-DavidLLMW #model checking #realtime #statistics: Time for Statistical Model Checking of Real-Time Systems (AD, KGL, AL, MM, ZW), pp. 349–355.
CAV-2011-DudkaPV #data type #logic #named #using: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic (KD, PP, TV), pp. 372–378.
CAV-2011-HagueL #data type #model checking #recursion #source code: Model Checking Recursive Programs with Numeric Data Types (MH, AWL), pp. 743–759.
CAV-2011-KroeningOSWW #bound #linear #model checking: Linear Completeness Thresholds for Bounded Model Checking (DK, JO, OS, TW, JW), pp. 557–572.
CAV-2011-MorbePS #automaton #model checking: Fully Symbolic Model Checking for Timed Automata (GM, FP, CS), pp. 616–632.
ICLP-2011-ZomboriCS #functional #prolog #static typing #type checking: Static Type Checking for the Q Functional Language in Prolog (ZZ, JC, PS), pp. 62–72.
ICLP-J-2011-HallerstedeL #concurrent #constraints #specification: Constraint-based deadlock checking of high-level specifications (SH, ML), pp. 767–782.
ICST-2011-KeatingMH #implementation #model checking: Model Checking a TTCAN Implementation (DK, AM, MPH), pp. 387–396.
ICST-2011-SchulerZ #quality: Assessing Oracle Quality with Checked Coverage (DS, AZ), pp. 90–99.
ICST-2011-ZhouF #database: Inferential Checking for Mutants Modifying Database States (CZ, PGF), pp. 259–268.
LICS-2011-Kobayashi #higher-order #model checking #theory and practice: Higher-Order Model Checking: From Theory to Practice (NK0), pp. 219–224.
TAP-2011-BentakoukPZ #behaviour #consistency #smt #testing #web #web service: Checking the Behavioral Conformance of Web Services with Symbolic Testing and an SMT Solver (LB, PP, FZ), pp. 33–50.
TAP-2011-Gaudel #modelling #proving #source code #testing: Checking Models, Proving Programs, and Testing Systems (MCG), pp. 1–13.
VMCAI-2011-Bradley #model checking #satisfiability: SAT-Based Model Checking without Unrolling (ARB), pp. 70–87.
VMCAI-2011-DonaldsonHK #lightweight #static analysis: Strengthening Induction-Based Race Checking with Lightweight Static Analysis (AFD, LH, DK), pp. 169–183.
VMCAI-2011-LopesR #distributed #model checking #predict: Distributed and Predictable Software Model Checking (NPL, AR), pp. 340–355.
ASE-2010-HalleEBB #fault #model checking #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 #model checking #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 #model checking #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 #model checking #precise #representation: Model checking graph representation of precise boolean inter-procedural flow analysis (DL), pp. 511–516.
ASE-2010-NgocO #fault #using: Checking roundoff errors using counterexample-guided narrowing (DTBN, MO), pp. 301–304.
ASE-2010-VierhauserGERH #consistency #flexibility #modelling #product line #scalability #variability: Flexible and scalable consistency checking on product line variability models (MV, PG, AE, RR, WH), pp. 63–72.
CASE-2010-BeringV #automation #framework #quality #statistics: A Quality Framework to check the applicability of engineering and statistical assumptions for automated gauges (TPKB, SCV), pp. 319–325.
DAC-2010-ChocklerKP #model checking: Coverage in interpolation-based model checking (HC, DK, MP), pp. 182–187.
DAC-2010-HorowitzJLLLM #analysis #equivalence #modelling: Fortifying analog models with equivalence checking and coverage analysis (MH, MJ, FL, SL, BL, JM), pp. 425–430.
DAC-2010-LimKH #functional #generative #modelling #performance: An efficient test vector generation for checking analog/mixed-signal functional models (BL, JK, MAH), pp. 767–772.
DAC-2010-ThalmaierNWSBK #induction #invariant #satisfiability: Analyzing k-step induction to compute invariants for SAT-based property checking (MT, MDN, MW, DS, JB, WK), pp. 176–181.
DATE-2010-HaoXRY #behaviour #equivalence #optimisation #synthesis: Optimizing equivalence checking for behavioral synthesis (KH, FX, SR, JY), pp. 1500–1505.
DATE-2010-RaffelsieperMS #library: Checking and deriving module paths in Verilog cell library descriptions (MR, MRM, CWHS), pp. 1506–1511.
FASE-2010-GroherRE #consistency #constraints #incremental: Incremental Consistency Checking of Dynamic Constraints (IG, AR, AE), pp. 203–217.
FASE-2010-LehnerM #performance #runtime: Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups (HL, PM), pp. 338–352.
FoSSaCS-2010-DemriS #decidability #ltl #model checking: When Model-Checking Freeze LTL over Counter Machines Becomes Decidable (SD, AS), pp. 176–190.
FoSSaCS-2010-NielsonN #logic #model checking #static analysis: Model Checking Is Static Analysis of Modal Logic (FN, HRN), pp. 191–205.
FoSSaCS-2010-ToL #algorithm #decidability #infinity #ltl #model checking: Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems (AWT, LL), pp. 221–236.
TACAS-2010-BaslerHKOWZ #model checking #named: Boom: Taking Boolean Program Model Checking One Step Further (GB, MH, DK, CHLO, TW, HZ), pp. 145–149.
TACAS-2010-FogartyV #automaton #performance: Efficient Büchi Universality Checking (SF, MYV), pp. 205–220.
TACAS-2010-MalinowskiN #automaton #bound #model checking #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: Model Checking Interactive Markov Chains (LZ, MRN), pp. 53–68.
CSMR-2010-LuciaDGR #behaviour #design pattern #detection #model checking: Improving Behavioral Design Pattern Detection through Model Checking (ADL, VD, CG, MR), pp. 176–185.
ICPC-2010-BeyerF10a #dependence #named: CheckDep: A Tool for Tracking Software Dependencies (DB, AF), pp. 42–43.
ICSM-2010-Letarte #interprocedural #model checking #performance #static analysis: Conversion of fast inter-procedural static analysis to model checking (DL), pp. 1–2.
ICSM-2010-ZhangSZ #automation: Automatic checking of license compliance (HZ, BS, LZ), pp. 1–3.
WCRE-2010-Bittencourt #consistency #evolution: Conformance Checking during Software Evolution (RAB), pp. 289–292.
PLDI-2010-KhooCF #execution #symbolic computation #type checking: Mixing type checking and symbolic execution (YPK, BYEC, JSF), pp. 436–447.
PLDI-2010-RuwaseCGM #correctness #optimisation #tool support: Decoupled lifeguards: enabling path optimizations for dynamic correctness checking tools (OR, SC, PBG, TCM), pp. 25–35.
PLDI-2010-TorlakVD #axiom #memory management #modelling #named #specification: MemSAT: checking axiomatic specifications of memory models (ET, MV, JD), pp. 341–350.
FLOPS-2010-BartheBK #framework #functional: A Functional Framework for Result Checking (GB, PB, CK), pp. 72–86.
ICALP-v2-2010-GollerHOW #automaton #model checking #parametricity: Model Checking Succinct and Parametric One-Counter Automata (SG, CH, JO, JW), pp. 575–586.
IFM-2010-Baier #distributed #model checking #on the #random: On Model Checking Techniques for Randomized Distributed Systems (CB), pp. 1–11.
IFM-2010-BouchenebIN #algorithm #model checking #replication: Symbolic Model-Checking of Optimistic Replication Algorithms (HB, AI, MN), pp. 89–104.
SEFM-2010-BenettiMV #ad hoc #model checking #network #protocol: Model Checking Ad Hoc Network Routing Protocols: ARAN vs. endairA (DB, MM, LV), pp. 191–202.
SEFM-2010-BersaniCFPR #constraints #integer #ltl #runtime #smt #specification #verification: SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability (MMB, LC, AF, MP, MR), pp. 244–254.
SEFM-2010-HussainL #ml #named #runtime #specification: temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties (FH, GTL), pp. 63–72.
SEFM-2010-LindsayWY #assessment #behaviour #model checking #safety #using: Safety Assessment Using Behavior Trees and Model Checking (PAL, KW, NY), pp. 181–190.
GT-VMT-2010-BlumeBK #graph #invariant: Recognizable Graph Languages for Checking Invariants (CB, HJSB, BK).
ICGT-2010-Ujhelyi #model transformation #source code #static typing #type checking: Static Type Checking of Model Transformation Programs (ZU), pp. 413–415.
CAiSE-2010-SidorovaST #concept #correctness #workflow: Workflow Soundness Revisited: Checking Correctness in the Presence of Data While Staying Conceptual (NS, CS, NT), pp. 530–544.
ICEIS-DISI-2010-ObermeierB #ad hoc #constraints #mobile #network #transaction: Constraint Checking for Non-blocking Transaction Processing in Mobile Ad-hoc Networks (SO, SB), pp. 166–175.
KDIR-2010-MollerEDS #automation #ontology #recognition #using: Automatic Spatial Plausibility Checks for Medical Object Recognition Results using a Spatio-anatomical Ontology (MM, PE, AD, DS), pp. 5–13.
SEKE-2010-AvilaSCY #comparison #constraints #ocl #runtime: Runtime Constraint Checking Approaches for OCL, A Critical Comparison (CA, AS, YC, CY), pp. 393–398.
SEKE-2010-Cao #automaton #interface #refinement: Refinement Checking for Interface Automata with Z Notation (ZC), pp. 399–404.
SEKE-2010-ElabdCH #approach #data access #implementation #web #web service: Selecting Web Services for Choreography Implementation: Compatibility Checking Approach with Access Control (EE, EC, MSH), pp. 235–240.
SEKE-2010-ZhangZH #model checking #precise: Some Improvements for More Precise Model Checking (ZZ, QZ, MH), pp. 106–112.
OOPSLA-2010-RobersonB #composition #model checking #performance: Efficient modular glass box software model checking (MR, CB), pp. 4–21.
TOOLS-EUROPE-2010-RenggliDGN #domain-specific language: Domain-Specific Program Checking (LR, SD, TG, ON), pp. 213–232.
GPCE-2010-MiaoS #incremental #metaprogramming: Incremental type-checking for type-reflective metaprograms (WM, JGS), pp. 167–176.
PPDP-2010-Bonacina #on the #proving #theorem proving: On theorem proving for program checking: historical perspective and recent developments (MPB), pp. 1–12.
PPDP-2010-Jeltsch #combinator #static typing #type checking: Generic record combinators with static type checking (WJ), pp. 143–154.
POPL-2010-MartinHCAC #c #c++ #concurrent #policy #source code: Dynamically checking ownership policies in concurrent c/c++ programs (JPM, MH, MC, PA, MC), pp. 457–470.
RE-2010-KamalrudinHG #approach #automation #consistency #named #nondeterminism #requirements #visual notation: MaramaAI: Automated and Visual Approach for Inconsistency Checking of Requirements (MK, JGH, JCG), pp. 393–394.
SAC-2010-Fellah #automaton #framework #model checking: Time and alternation: an automata based framework to software model checking (AF), pp. 2498–2502.
SAC-2010-Herold #architecture #component: Checking architectural compliance in component-based systems (SH), pp. 2244–2251.
SAC-2010-KerfootM #aspect-oriented #concurrent #contract: Checking concurrent contracts with aspects (EK, SM), pp. 2523–2530.
SAC-2010-SpinolaPT #approach #named #requirements: UbiCheck: an approach to support requirements definition in the ubicomp domain (ROS, FCRP, GHT), pp. 306–310.
SAC-2010-VogelsJP #generative #performance #proving #verification: A machine-checked soundness proof for an efficient verification condition generator (FV, BJ, FP), pp. 2517–2522.
ICSE-2010-ClassenHSLR #model checking #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 #model checking #multi #smt #thread: SMT-based bounded model checking for multi-threaded software in embedded systems (LC), pp. 373–376.
ICSE-2010-Marinho #consistency #modelling #ocl #product line #using: A proposal for consistency checking in dynamic software product line models using OCL (FGM), pp. 333–334.
ICSE-2010-Rakamaric #concurrent #named #source code: STORM: static unit checking of concurrent programs (ZR), pp. 519–520.
ISMM-2010-VechevYY #named #parallel: PHALANX: parallel checking of expressive heap assertions (MTV, EY, GY), pp. 41–50.
OSDI-2010-Chlipala #policy #security #static analysis: Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications (AC), pp. 105–118.
CAV-2010-CernyRZCA #concurrent #implementation #model checking: Model Checking of Linearizability of Concurrent List Implementations (PC, AR, DZ, SC, RA), pp. 465–479.
CAV-2010-FerranteMNPS #model checking: A NuSMV Extension for Graded-CTL Model Checking (AF, MM, MN, MP, FS), pp. 670–673.
CAV-2010-GrafPQ #distributed #model checking: Achieving Distributed Control through Model Checking (SG, DP, SQ), pp. 396–409.
CAV-2010-HerbreteauSW #automaton #performance: Efficient Emptiness Check for Timed Büchi Automata (FH, BS, IW), pp. 148–161.
CAV-2010-TorreMP #concurrent #interface #linear #model checking #source code #using: Model-Checking Parameterized Concurrent Programs Using Linear Interfaces (SLT, PM, GP), pp. 629–644.
ICST-2010-LodingP #automaton #generative #model checking #testing: Timed Moore Automata: Test Data Generation and Model Checking (HL, JP), pp. 449–458.
ICST-2010-PavlovicE #diagrams #model checking: Model Checking PLC Software Written in Function Block Diagram (OP, HDE), pp. 439–448.
SAT-2010-MillerKLB #bound #design #encoding #model checking: Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs (CM, SK, MDTL, BB), pp. 194–208.
VMCAI-2010-AminofKM #model checking: Improved Model Checking of Hierarchical Systems (BA, OK, AM), pp. 61–77.
VMCAI-2010-Dubrovin #bound #reachability: Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing (JD), pp. 146–162.
VMCAI-2010-Katoen #model checking #probability #roadmap: Advances in Probabilistic Model Checking (JPK), p. 25.
VMCAI-2010-SridharH #model checking #monitoring: Model-Checking In-Lined Reference Monitors (MS, KWH), pp. 312–327.
CBSE-2009-LiCHMC #component #fault tolerance #model checking: Selecting Fault Tolerant Styles for Third-Party Components with Model Checking Support (JL, XC, GH, HM, FC), pp. 69–86.
QoSA-2009-BiehlL #architecture #automation #consistency #development #modelling: Automated Architecture Consistency Checking for Model Driven Software Development (MB, WL), pp. 36–51.
ASE-2009-ArthoLHTY #branch #linear #model checking: 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 #model checking: Cluster-Based I/O-Efficient LTL Model Checking (JB, LB, PS), pp. 635–639.
ASE-2009-CavadaCMMMMPRST #requirements #validation: Supporting Requirements Validation: The EuRailCheck Tool (RC, AC, AM, CM, AM, SM, MP, MR, AS, ST), pp. 665–667.
ASE-2009-CordeiroFM #bound #embedded #model checking #smt: SMT-Based Bounded Model Checking for Embedded ANSI-C Software (LCC, BF, JMS), pp. 137–148.
ASE-2009-Kamalrudin #automation #consistency #nondeterminism #requirements #tool support: Automated Software Tool Support for Checking the Inconsistency of Requirements (MK), pp. 693–697.
ASE-2009-KimYS #concurrent #detection #heuristic #memory management #model checking #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 #model checking #product line: Model Checking of Domain Artifacts in Product Line Engineering (KL, KP, ST), pp. 269–280.
ASE-2009-SiddiquiMK #constraints #optimisation #performance #theorem proving: Optimizing a Structural Constraint Solver for Efficient Software Checking (JHS, DM, SK), pp. 615–619.
CASE-2009-VoronovA #model checking #process #using #verification: Verification of process operations using model checking (AV, KÅ), pp. 415–420.
DAC-2009-AbercrombiePC #design #equation #simulation: Use of lithography simulation for the calibration of equation-based design rule checks (DA, FP, CC), pp. 67–70.
DAC-2009-ChauhanGHMS #equivalence: Non-cycle-accurate sequential equivalence checking (PC, DG, GH, AM, NS), pp. 460–465.
DATE-2009-BaumgartnerM #liveness #scalability: Scalable liveness checking via property-preserving transformations (JB, HM), pp. 1680–1685.
DATE-2009-CabodiCGMNQ #constraints #model checking #verification: Speeding up model checking by exploiting explicit and hidden verification constraints (GC, PC, LG, MM, SN, SQ), pp. 1686–1691.
DATE-2009-DemangelFDCW #architecture: A generic architecture of CCSDS Low Density Parity Check decoder for near-earth applications (FD, NF, ND, FC, CW), pp. 1242–1245.
DATE-2009-KoelblJJP #equivalence: Solver technology for system-level to RTL equivalence checking (AK, RJ, HJ, CP), pp. 196–201.
DATE-2009-YanHL #detection #fault #online: A unified online Fault Detection scheme via checking of Stability Violation (GY, YH, XL), pp. 496–501.
DocEng-2009-VallePC #consistency #documentation #geometry #retrieval: Geometric consistency checking for local-descriptor based document retrieval (EV, DP, MC), pp. 135–138.
FoSSaCS-2009-BroadbentO #higher-order #model checking #on the #recursion: On Global Model Checking Trees Generated by Higher-Order Recursion Schemes (CHB, CHLO), pp. 107–121.
TACAS-2009-Miller #development #model checking #modelling: Bridging the Gap Between Model-Based Development and Model Checking (SPM), pp. 443–453.
TACAS-2009-NguyenR #garbage collection #model checking: Memoised Garbage Collection for Software Model Checking (VYN, TCR), pp. 201–214.
TACAS-2009-NoriRTT #static analysis #testing: The YogiProject: Software Property Checking via Static Analysis and Testing (AVN, SKR, ST, AVT), pp. 178–181.
TACAS-2009-WehrleKP #model checking: Transition-Based Directed Model Checking (MW, SK, AP), pp. 186–200.
ICSM-2009-YangDR #model checking: Regression model checking (GY, MBD, GR), pp. 115–124.
SCAM-2009-AchenbachO #abstraction #model checking #testing: Engineering Abstractions in Model Checking and Testing (MA, KO), pp. 137–146.
PEPM-2009-RungtaM #model checking #morphism #polymorphism #source code: Guided model checking for programs with polymorphism (NR, EGM), pp. 21–30.
PEPM-2009-SalamaMTGO #consistency #dependent type #using: Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions (CS, GM, WT, JG, JO), pp. 121–130.
PLDI-2009-AftandilianG #garbage collection #using: GC assertions: using the garbage collector to check heap properties (EA, SZG), pp. 235–244.
SAS-2009-GodoyT #invariant #source code: Invariant Checking for Programs with Procedure Calls (GG, AT), pp. 326–342.
SAS-2009-NiedzielskiRGP #bound #constraints #control flow: A Verifiable, Control Flow Aware Constraint Analyzer for Bounds Check Elimination (DN, JvR, AG, KP), pp. 137–153.
SAS-2009-WehrleH #graph #model checking: The Causal Graph Revisited for Directed Model Checking (MW, MH), pp. 86–101.
CIAA-2009-CourbisHK #approximate #model checking: TAGED Approximations for Temporal Properties Model-Checking (RC, PCH, OK), pp. 135–144.
ICALP-v2-2009-KobayashiO #calculus #complexity #model checking #recursion #μ-calculus: Complexity of Model Checking Recursion Schemes for Fragments of the Modal μ-Calculus (NK, CHLO), pp. 223–234.
ICALP-v2-2009-KuhtzF #ltl: LTL Path Checking Is Efficiently Parallelizable (LK, BF), pp. 235–246.
FM-2009-LiuCLS #model checking #refinement: Model Checking Linearizability via Refinement (YL, WC, YAL, JS), pp. 321–337.
FM-2009-PradellaMP #bound #encoding #metric #model checking: A Metric Encoding for Bounded Model Checking (MP, AM, PSP), pp. 741–756.
FM-2009-ShaoKP #approach #bound #formal method #incremental #lightweight #using: An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method (DS, SK, DEP), pp. 757–772.
FM-2009-SunLRLD #abstraction #model checking #process: Fair Model Checking with Process Counter Abstraction (JS, YL, AR, SL, JSD), pp. 123–139.
FM-2009-Tonetta #abstraction #model checking: Abstract Model Checking without Computing the Abstraction (ST), pp. 89–105.
IFM-2009-VargasGTG #ltl #model checking: Model Checking LTL Formulae in RAISE with FDR (APV, AGG, SLTT, CG), pp. 231–245.
IFM-2009-YangASHSG #model checking #reduction: Dynamic Path Reduction for Software Model Checking (ZY, BAR, KAS, XH, SAS, RG), pp. 322–336.
SEFM-2009-BertoliniM #model checking #probability #testing #user interface #using: Using Probabilistic Model Checking to Evaluate GUI Testing Techniques (CB, AM), pp. 115–124.
SEFM-2009-BuiN #heuristic #model checking: Heuristic Sensitivity in Guided Random-Walk Based Model Checking (THB, AN), pp. 125–134.
SEFM-2009-HieronsJUY #adaptation #sequence #using: Checking Sequence Construction Using Adaptive and Preset Distinguishing Sequences (RMH, GVJ, HU, HY), pp. 157–166.
SEFM-2009-KawamataSIH #refinement #specification: Specifying and Checking Refinement Relationships in VDM++ (YK, CS, FI, SH), pp. 220–227.
SEFM-2009-NgocO #analysis #fault #model checking: Overflow and Roundoff Error Analysis via Model Checking (DTBN, MO), pp. 105–114.
CEFP-2009-Hughes #quickcheck #testing: Software Testing with QuickCheck (JH), pp. 183–223.
ICFP-2009-ClaessenPSHSAW #erlang #quickcheck: Finding race conditions in Erlang with QuickCheck and PULSE (KC, MHP, NS, JH, HS, TA, UTW), pp. 149–160.
AdaEurope-2009-BuchsLC #generative #model checking #modelling #process #testing: Model Checking Techniques for Test Generation from Business Process Models (DB, LL, AC), pp. 59–74.
EDOC-2009-DeitersDHR #architecture #enterprise #rule-based: Rule-Based Architectural Compliance Checks for Enterprise Architecture Management (CD, PD, SH, AR), pp. 183–192.
ECOOP-2009-BierhoffBA #api #protocol: Practical API Protocol Checking with Access Permissions (KB, NEB, JA), pp. 195–219.
ECOOP-2009-JaspanA #framework #interactive: Checking Framework Interactions with Relationships (CJ, JA), pp. 27–51.
PPDP-2009-GuoZS #consistency #named: L2C2: logic-based LSC consistency checking (HFG, WZ, MS), pp. 183–194.
PPDP-2009-Kobayashi #higher-order #model checking: Model-checking higher-order functions (NK), pp. 25–36.
POPL-2009-BrunelDHLM #logic #model checking #using: A foundation for flow-based program matching: using temporal logic and model checking (JB, DD, RRH, JLL, GM), pp. 114–126.
POPL-2009-ConditHLQ #low level #type checking: Unifying type checking and property checking for low-level code (JC, BH, SKL, SQ), pp. 302–314.
POPL-2009-XuJC #contract #haskell: Static contract checking for Haskell (DNX, SLPJ, KC), pp. 41–52.
SAC-2009-CasadeiV #design #model checking #probability #self #simulation #using: Using probabilistic model checking and simulation for designing self-organizing systems (MC, MV), pp. 2103–2104.
SAC-2009-GroppeNL #java #named #query #rdf #satisfiability #semantics #type safety #web: SWOBE — embedding the semantic web languages RDF, SPARQL and SPARUL into java for guaranteeing type safety, for checking the satisfiability of queries and for the determination of query result types (SG, JN, VL), pp. 1239–1246.
SAC-2009-Hurlin #parallel #protocol #specification #thread: Specifying and checking protocols of multithreaded classes (CH), pp. 587–592.
SAC-2009-JamesC #ml #multi #static analysis: Extended static checking in JML4: benefits of multiple-prover support (PRJ, PC), pp. 609–614.
ESEC-FSE-2009-BurnimS #parallel #source code #thread: Asserting and checking determinism for multithreaded programs (JB, KS), pp. 3–12.
ESEC-FSE-2009-DelawareCB #composition: Fitting the pieces together: a machine-checked model of safe composition (BD, WRC, DSB), pp. 243–252.
ICSE-2009-HangalL #automation #object-oriented #source code: Automatic dimension inference and checking for object-oriented programs (SH, MSL), pp. 155–165.
CGO-2009-YuGS #fault tolerance #named: ESoftCheck: Removal of Non-vital Checks for Fault Tolerance (JY, MJG, MS), pp. 35–46.
CAV-2009-BasuBPS #distributed #model checking #scheduling: Priority Scheduling of Distributed Systems Based on Model Checking (AB, SB, DP, JS), pp. 79–93.
CAV-2009-VerdoolaegeJB #equivalence #source code #using: Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences (SV, GJ, MB), pp. 599–613.
CSL-2009-GuoWXC #model checking #on the: On Model Checking Boolean BI (HG, HW, ZX, YC), pp. 302–316.
CSL-2009-HofmannR #analysis #performance: Efficient Type-Checking for Amortised Heap-Space Analysis (MH, DR), pp. 317–331.
CSL-2009-To #model checking #process: Model Checking FO(R) over One-Counter Processes and beyond (AWT), pp. 485–499.
ICLP-2009-MeraLH #framework #runtime #testing #verification: Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework (EM, PLG, MVH), pp. 281–295.
ICST-2009-MurphySK #ml #runtime #testing #using: Using JML Runtime Assertion Checking to Automate Metamorphic Testing in Applications without Test Oracles (CM, KS, GEK), pp. 436–445.
ICST-2009-PostS #bound #equivalence #functional #implementation #model checking #proving #using: Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking (HP, CS), pp. 31–40.
ISSTA-2009-SchulerDZ #invariant #mutation testing #performance #testing: Efficient mutation testing by checking invariant violations (DS, VD, AZ), pp. 69–80.
LICS-2009-ChenHKM #automaton #markov #model checking #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 #model checking #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 #model checking #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 #model checking #symbolic computation: Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables (NR), pp. 137–152.
TestCom-FATES-2009-WieczorekKRLBPS #integration #model checking #modelling #testing: Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models (SW, VK, AR, ML, JB, DP, IS), pp. 179–194.
TLCA-2009-AbelCP #algorithm #composition #proving #type system: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (AA, TC, MP), pp. 5–19.
VMCAI-2009-Emerson #model checking #problem: Model Checking: Progress and Problems (EAE), p. 1.
VMCAI-2009-GallowayLMS #file system #linux #model checking: Model-Checking the Linux Virtual File System (AG, GL, JTM, RS), pp. 74–88.
VMCAI-2009-GodefroidP #ltl #model checking #revisited: LTL Generalized Model Checking Revisited (PG, NP), pp. 89–104.
VMCAI-2009-Gupta #concurrent #model checking #source code: Model Checking Concurrent Programs (AG), p. 2.
VMCAI-2009-Oshman #bound #model checking: An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking (RO), pp. 275–289.
VMCAI-2009-WimmerBB #bound #generative #markov #model checking #using: Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking (RW, BB, BB), pp. 366–380.
CBSE-2008-BothZ #automation #component #consistency #parallel #protocol #recursion: Automatic Protocol Conformance Checking of Recursive and Parallel Component-Based Systems (AB, WZ), pp. 163–179.
CBSE-2008-VarekovaC #component #model checking: Model Checking of Control-User Component-Based Parametrised Systems (PV, IC), pp. 146–162.
QoSA-2008-GallottiGMT #composition #model checking #predict #probability #quality: Quality Prediction of Service Compositions through Probabilistic Model Checking (SG, CG, RM, GT), pp. 119–134.
ASE-2008-HartKGCL08a #model checking #named #proving: PtYasm: Software Model Checking with Proof Templates (TEH, KK, AG, MC, DL), pp. 479–480.
ASE-2008-JoshiS #java #parallel #predict #source code #thread #type system: Predictive Typestate Checking of Multithreaded Java Programs (PJ, KS), pp. 288–296.
ASE-2008-KastnerA #approach #formal method #product line: Type-Checking Software Product Lines — A Formal Approach (CK, SA), pp. 258–267.
ASE-2008-PostSKG #abstract interpretation #bound #model checking: Reducing False Positives by Combining Abstract Interpretation and Bounded Model Checking (HP, CS, AK, TG), pp. 188–197.
ASE-2008-PradellaMP #bound #realtime #satisfiability #specification: Refining Real-Time System Specifications through Bounded Model- and Satisfiability-Checking (MP, AM, PSP), pp. 119–127.
DAC-2008-MohalikRDRSPJ #analysis #embedded #latency #model checking #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.
DAC-2008-UrardMGC #equivalence: Leveraging sequential equivalence checking to enable system-level to RTL flows (PU, AM, RG, NC), pp. 816–821.
DATE-2008-DongZ #integration #logic #standard #synthesis: Logic Synthesis with Nanowire Crossbar: Reality Check and Standard Cell-based Integration (MD, LZ), pp. 268–271.
DATE-2008-FeinsteinTM #detection #equivalence #logic #using: Partially Redundant Logic Detection Using Symbolic Equivalence Checking in Reversible and Irreversible Logic Circuits (DYF, MAT, DMM), pp. 1378–1381.
DATE-2008-SteinhorstH #model checking #specification #using: Model Checking of Analog Systems using an Analog Specification Language (SS, LH), pp. 324–329.
SIGMOD-2008-ChakrabartiCGX #approximate #performance: An efficient filter for approximate membership checking (KC, SC, VG, DX), pp. 805–818.
VLDB-2008-DeutchM #execution #query #type checking #type inference: Type inference and type checking for queries on execution traces (DD, TM), pp. 352–363.
FASE-2008-FantechiGLMPT #approach #model checking #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: Model-Checking ω-Regular Properties of Interval Markov Chains (KC, KS, TAH), pp. 302–317.
FoSSaCS-2008-DemriLS #automaton #ltl #model checking: Model Checking Freeze LTL over One-Counter Automata (SD, RL, AS), pp. 490–504.
TACAS-2008-BakewellG #game studies #model checking #on the fly: On-the-Fly Techniques for Game-Based Software Model Checking (AB, DRG), pp. 78–92.
TACAS-2008-BarnatBSW #ltl #model checking: Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking (JB, LB, PS, MW), pp. 48–62.
TACAS-2008-CaniartFLZ #model checking: Accelerating Interpolation-Based Model-Checking (NC, EF, JL, MZ), pp. 428–442.
TACAS-2008-ClarkeTV #abstraction #concurrent #framework #model checking #proving: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems (EMC, MT, HV), pp. 33–47.
TACAS-2008-FinkbeinerPS #composition #model checking #named #synthesis: RESY: Requirement Synthesis for Compositional Model Checking (BF, HJP, SS), pp. 463–466.
TACAS-2008-KatzP #model checking #programming #search-based: Model Checking-Based Genetic Programming with an Application to Mutual Exclusion (GK, DP), pp. 141–156.
TACAS-2008-KupferschmidHL #abstraction #model checking #performance: Fast Directed Model Checking Via Russian Doll Abstraction (SK, JH, KGL), pp. 203–217.
TACAS-2008-Moskal #proving #smt: Rocket-Fast Proof Checking for SMT Solvers (MM), pp. 486–500.
TACAS-2008-PaceS #model checking #visualisation: Computation and Visualisation of Phase Portraits for Model Checking SPDIs (GJP, GS), pp. 341–345.
TACAS-2008-SankaranarayananDI #hybrid #model checking #using: Symbolic Model Checking of Hybrid Systems Using Template Polyhedra (SS, TD, FI), pp. 188–202.
TACAS-2008-WulfDMR #algorithm #anti #ltl #model checking #named #satisfiability: Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking (MDW, LD, NM, JFR), pp. 63–77.
CSMR-2008-KnodelMHM #architecture #case study #experience #industrial: Architecture Compliance Checking — Experiences from Successful Technology Transfer to Industry (JK, DM, UH, GM), pp. 43–52.
CSMR-2008-TsantalisCC #identification #named #smell: JDeodorant: Identification and Removal of Type-Checking Bad Smells (NT, TC, AC), pp. 329–331.
ICSM-2008-KnodelMR #architecture #empirical #feedback: Constructive architecture compliance checking — an experiment on support by live feedback (JK, DM, DR), pp. 287–296.
SCAM-2008-WangZZ #automation #detection #model checking #program analysis: Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking (LW, QZ, PZ), pp. 165–173.
PEPM-2008-PopeeaXC #array #bound #precise: A practical and precise inference and specializer for array bound checks elimination (CP, DNX, WNC), pp. 177–187.
PLDI-2008-AndersonGEB #c #named #parallel #thread: SharC: checking data sharing strategies for multithreaded C (ZRA, DG, RE, EAB), pp. 149–158.
PLDI-2008-GuerraouiHJS #model checking #transaction: Model checking transactional memories (RG, TAH, BJ, VS), pp. 372–382.
PLDI-2008-MusuvathiQ #model checking: Fair stateless model checking (MM, SQ), pp. 362–371.
PLDI-2008-Terauchi #linear #programming: Checking race freedom via linear programming (TT), pp. 1–10.
STOC-2008-GoldwasserGHKR #approach: A (de)constructive approach to program checking (SG, DG, AH, TK, GNR), pp. 143–152.
FLOPS-2008-ChristiansenF #for free #named #testing: EasyCheck — Test Data for Free (JC, SF), pp. 322–336.
ICALP-B-2008-BouyerMOW #complexity #model checking #on the #realtime: On Expressiveness and Complexity in Real-Time Model Checking (PB, NM, JO, JW), pp. 124–135.
LATA-2008-ChampavereGLN #automaton #performance: Efficient Inclusion Checking for Deterministic Tree Automata and DTDs (JC, RG, AL, JN), pp. 184–195.
FM-2008-AmtoftHRRHG #contract #data flow #specification: Specification and Checking of Software Contracts for Conditional Information Flow (TA, JH, ER, R, JH, DG), pp. 229–245.
FM-2008-ChalinR #fault #ml #performance #runtime #using: JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity (PC, FR), pp. 246–261.
FM-2008-Engler #case study #experience #lessons learnt #scalability: Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real Systems (DRE), p. 33.
FM-2008-MateescuT #concurrent #model checking: A Model Checking Language for Concurrent Value-Passing Systems (RM, DT), pp. 148–164.
FM-2008-RudichDM #specification: Checking Well-Formedness of Pure-Method Specifications (AR, ÁD, PM), pp. 68–83.
SEFM-2008-EdelkampS #ltl #model checking: Flash-Efficient LTL Model Checking with Minimal Counterexamples (SE, DS), pp. 73–82.
SEFM-2008-FranzleH #approximate #calculus #model checking #performance: Efficient Model Checking for Duration Calculus Based on Branching-Time Approximations (MF, MRH), pp. 63–72.
SEFM-2008-TruongTHNTH #aspect-oriented #interactive #interface #programming #protocol #using: Checking Interface Interaction Protocols Using Aspect-Oriented Programming (AHT, TBT, DVH, VHN, NTTT, PDH), pp. 382–386.
ICFP-2008-AdamsD #graph #performance #similarity: Efficient nondestructive equality checking for trees and graphs (MDA, RKD), pp. 179–188.
ICFP-2008-SchrijversJCS #type checking: Type checking with open type functions (TS, SLPJ, MMTC, MS), pp. 51–62.
GT-VC-2007-BaresiRRS08 #graph transformation #model checking #performance: An Efficient Solution for Model Checking Graph Transformation Systems (LB, VR, ATR, PS), pp. 3–21.
GT-VMT-2008-AzabP #c++ #graph #source code #type checking: Type Checking C++ Template Instantiation by Graph Programs (KA, KHP).
ICEIS-AIDSS-2008-LampertiVZ #on the #similarity: On Checking Temporal-Observation Subsumption in Similarity-Based Diagnosis of Active Systems (GL, FV, MZ), pp. 44–53.
ICEIS-ISAS1-2008-MoralesTPA #communication #composition #concept #model checking #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 #model checking #verification: Compositional Model-Checking Verification of Critical Systems (LEMM, MIC, MAP, KBA), pp. 213–225.
CIKM-2008-LinL #clique #mining #performance: Fast spatial co-location mining without cliqueness checking (ZL, SL), pp. 1461–1462.
CIKM-2008-PlacekTSDS #approach #heuristic #query: A heuristic approach for checking containment of generalized tree-pattern queries (PP, DT, SS, TD, TKS), pp. 551–560.
ICPR-2008-DingSK #recognition: A new courtesy amount recognition module of a Check Reading System (WD, CYS, AK), pp. 1–4.
SEKE-2008-ParkK #automaton #bound #constraints #lts #model checking #using: Using Boolean Cardinality Constraint for LTS Bounded Model Checking (SP, GK), pp. 537–542.
SEKE-2008-SloanK #model checking #towards #web #web service: Toward Model Checking Web Services Over the Web (JCS, TMK), pp. 519–524.
MoDELS-2008-WaignierSMD #component #framework #interactive #modelling: A Model-Based Framework for Statically and Dynamically Checking Component Interactions (GW, PS, AFLM, LD), pp. 371–385.
MoDELS-2008-WaignierSMD #component #framework #interactive #modelling: A Model-Based Framework for Statically and Dynamically Checking Component Interactions (GW, PS, AFLM, LD), pp. 371–385.
OOPSLA-2008-RobersonHDB #model checking #performance #type system: Efficient software model checking of soundness of type systems (MR, MH, PTD, CB), pp. 493–504.
TOOLS-EUROPE-2008-ArthoLHT #model checking #performance: Efficient Model Checking of Networked Applications (CA, WL, MH, YT), pp. 22–40.
PPDP-2008-DeckerM #consistency #nondeterminism: Classifying integrity checking methods with regard to inconsistency tolerance (HD, DM), pp. 195–204.
QAPL-2008-FaellaLS #linear #logic #model checking: Model Checking Quantitative Linear Time Logic (MF, AL, MS), pp. 61–77.
PADL-2008-Marpons-UceroMCHMF #automation #consistency #logic programming #using: Automatic Coding Rule Conformance Checking Using Logic Programming (GMU, JMC, MC, ÁHN, JJMN, LÅF), pp. 18–34.
RE-2008-LauenrothP #consistency #product line #requirements: Dynamic Consistency Checking of Domain Requirements in Product Line Engineering (KL, KP), pp. 193–202.
SAC-2008-FilhoZ #traceability: Traceability and completeness checking for agent-oriented systems (GACF, AZ), pp. 71–77.
SAC-2008-HieronsJUY #adaptation #sequence #using: Using adaptive distinguishing sequences in checking sequence constructions (RMH, GVJ, HU, HY), pp. 682–687.
SAC-2008-RamosSM #composition #consistency #framework #refinement: Framework composition conformance via refinement checking (RR, AS, AM), pp. 119–125.
SAC-2008-RuiWFKZ #architecture #control flow: Control flow checking and recovering based on 8051 architecture (RG, WC, FL, KD, ZW), pp. 1550–1551.
SAC-2008-ZarvicWE #modelling: Checking the alignment of value-based business models and IT functionality (NZ, RW, PvE), pp. 607–613.
ICSE-2008-BabicH #named #precise #scalability #static analysis: Calysto: scalable and precise extended static checking (DB, AJH), pp. 211–220.
ICSE-2008-EichbergKKM #dependence: Defining and continuous checking of structural program dependencies (ME, SK, KK, MM), pp. 391–400.
ICSE-2008-HuynhCSS #automation #composition #consistency: Automatic modularity conformance checking (SH, YC, YS, KJS), pp. 411–420.
ICSE-2008-SabetzadehNEC #consistency #distributed #modelling: Global consistency checking of distributed models with TReMer+ (MS, SN, SME, MC), pp. 815–818.
LDTA-2007-BouwersBV08 #grammarware #precedence: Grammar Engineering Support for Precedence Rule Recovery and Compatibility Checking (EB, MB, EV), pp. 85–101.
ASPLOS-2008-NightingalePCF #hardware #security: Parallelizing security checks on commodity hardware (EBN, DP, PMC, JF), pp. 308–318.
CGO-2008-BoissinotHGDR #liveness #performance #source code: Fast liveness checking for ssa-form programs (BB, SH, DG, BDdD, FR), pp. 35–44.
CGO-2008-SundaresanSR #exception: Removing redundancy via exception check motion (VS, MGS, PR), pp. 134–143.
HPCA-2008-ChenMP #constraints #graph #memory management #runtime #using #validation: Runtime validation of memory ordering using constraint graph checking (KC, SM, PP), pp. 415–426.
PPoPP-2008-VakkalankaSGK #model checking #named #source code: ISP: a tool for model checking MPI programs (SSV, SS, GG, RMK), pp. 285–286.
CAV-2008-Bjesse #approach #industrial #model checking #word: A Practical Approach to Word Level Model Checking of Industrial Netlists (PB), pp. 446–458.
CAV-2008-EdelkampSS #ltl #model checking: Semi-external LTL Model Checking (SE, PS, PS), pp. 530–542.
CAV-2008-Legay #model checking: T(O)RMC: A Tool for (ω)-Regular Model Checking (AL), pp. 548–551.
CAV-2008-NiebertPP #model checking: Discriminative Model Checking (PN, DP, AP), pp. 504–516.
CSL-2008-NakazawaTKN #λ-calculus: Undecidability of Type-Checking in Domain-Free Typed λ-Calculi with Existence (KN, MT, YK, HN), pp. 478–492.
ICLP-2008-Tsitovich #detection #model checking #security #using: Detection of Security Vulnerabilities Using Guided Model Checking (AT), pp. 822–823.
ICST-2008-KimCKK #model checking: Pre-testing Flash Device Driver through Model Checking Techniques (MK, YC, YK, HK), pp. 475–484.
IJCAR-2008-DarvasMR #performance: Efficient Well-Definedness Checking (ÁD, FM, AR), pp. 100–115.
IJCAR-2008-GhilardiNRZ #model checking #smt #towards: Towards SMT Model Checking of Array-Based Systems (SG, EN, SR, DZ), pp. 67–82.
LICS-2008-BaierBBBG #automaton #infinity #model checking: Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata (CB, NB, PB, TB, MG), pp. 217–226.
RTA-2008-EscobarMS #effectiveness #finite: Effectively Checking the Finite Variant Property (SE, JM, RS), pp. 79–93.
TAP-2008-Cao #equivalence #finite #higher-order #π-calculus: Equivalence Checking for a Finite Higher Order π-Calculus (ZC), pp. 30–47.
TAP-2008-VelroyenR #imperative #source code: Non-termination Checking for Imperative Programs (HV, PR), pp. 154–170.
TestCom-FATES-2008-SimaoP #finite #generative #sequence #state machine: Generating Checking Sequences for Partial Reduced Finite State Machines (AdSS, AP), pp. 153–168.
VMCAI-2008-DSilvaPK #approximate #model checking #refinement: Approximation Refinement for Interpolation-Based Model Checking (VD, MP, DK), pp. 68–82.
VMCAI-2008-FecherH #abstraction #model checking: Model Checking for Action Abstraction (HF, MH), pp. 112–126.
VMCAI-2008-GroceJ #dynamic analysis #model checking: Extending Model Checking with Dynamic Analysis (AG, RJ), pp. 142–156.
VMCAI-2008-Moy #composition: Sufficient Preconditions for Modular Assertion Checking (YM), pp. 188–202.
VMCAI-2008-NguyenKC #logic #runtime: Runtime Checking for Separation Logic (HHN, VK, WNC), pp. 203–217.
WICSA-2007-KnodelP #architecture #comparison: A Comparison of Static Architecture Compliance Checking Approaches (JK, DP), p. 12.
ASE-2007-Abi-AntounWT #consistency #data flow #diagrams #implementation #modelling #security: Checking threat modeling data flow diagrams for implementation conformance and security (MAA, DW, PT), pp. 393–396.
ASE-2007-ArmandoBCMS #model checking: The eureka tool for software model checking (AA, MB, DC, JM, PS), pp. 541–542.
ASE-2007-LauenrothP #automation #consistency #product line #requirements #specification #towards: Towards automated consistency checks of product line requirements specifications (KL, KP), pp. 373–376.
ASE-2007-TkachukR #composition #generative #model checking #slicing: Combining environment generation and slicing for modular software model checking (OT, SPR), pp. 401–404.
ASE-2007-WitkowskiBKW #concurrent #linux #model checking: Model checking concurrent linux device drivers (TW, NB, DK, GW), pp. 501–504.
DAC-2007-GuHY #distributed #embedded #model checking #optimisation: Optimization of Static Task and Bus Access Schedules for Time-Triggered Distributed Embedded Systems with Model-Checking (ZG, XH, MY), pp. 294–299.
DAC-2007-KoelblBP #equivalence #memory management #modelling: Memory Modeling in ESL-RTL Equivalence Checking (AK, JRB, CP), pp. 205–209.
DATE-2007-CabodiNQ #induction #invariant #model checking: Boosting the role of inductive invariants in model checking (GC, SN, SQ), pp. 1319–1324.
DATE-2007-GrosseKD #bound #functional #model checking: Estimating functional coverage in bounded model checking (DG, UK, RD), pp. 1176–1181.
DATE-2007-KhanA #architecture #configuration management #implementation #pipes and filters #programmable #realtime: Pipelined implementation of a real time programmable encoder for low density parity check code on a reconfigurable instruction cell architecture (ZK, TA), pp. 349–354.
DATE-2007-MoonBP #approach #composition #equivalence: A compositional approach to the combination of combinational and sequential equivalence checking of circuits without known reset states (IHM, PB, CP), pp. 1170–1175.
ICDAR-2007-MelloBZM #algorithm #performance: An Efficient Thresholding Algorithm for Brazilian Bank Checks (CABM, BLDB, CZ, VM), pp. 193–197.
ICDAR-2007-Shapiro #how #image #question: How to Reduce the Size of Bank Check Image Archive? (VS), pp. 148–152.
ICDAR-2007-ZiaratbanFE: Use of Legal Amount to Confirm or Correct the Courtesy Amount on Farsi Bank Checks (MZ, KF, ME), pp. 1123–1127.
ITiCSE-2007-OechsleB #automation #concurrent #thread: Checking automatically the output of concurrent threads (RO, KB), pp. 43–47.
WRLA-2006-NeuhausserN07 #abstraction #erlang #maude #model checking #source code: Abstraction and Model Checking of Core Erlang Programs in Maude (MRN, TN), pp. 147–163.
FoSSaCS-2007-BouyerLM #automaton #model checking: Model-Checking One-Clock Priced Timed Automata (PB, KGL, NM), pp. 108–122.
FoSSaCS-2007-FerranteM #calculus #μ-calculus: Enriched μ-Calculi Module Checking (AF, AM), pp. 183–197.
TACAS-2007-AbdullaDHR #model checking #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: Model Checking on Trees with Path Equivalences (RA, PC, SC), pp. 664–678.
TACAS-2007-AmlaM #abstraction #model checking #refinement #satisfiability: Combining Abstraction Refinement and SAT-Based Model Checking (NA, KLM), pp. 405–419.
TACAS-2007-BattBW #liveness #model checking #network #search-based: Model Checking Liveness Properties of Genetic Regulatory Networks (GB, CB, RW), pp. 323–338.
TACAS-2007-DoyenR #algorithm #approach #model checking: Improved Algorithms for the Automata-Based Approach to Model-Checking (LD, JFR), pp. 451–465.
TACAS-2007-EtessamiKVY #markov #model checking #multi #process: Multi-objective Model Checking of Markov Decision Processes (KE, MZK, MYV, MY), pp. 50–65.
TACAS-2007-HanK #model checking #probability: Counterexamples in Probabilistic Model Checking (TH, JPK), pp. 72–86.
TACAS-2007-JurdzinskiLS #automaton #model checking #probability: Model Checking Probabilistic Timed Automata with One or Two Clocks (MJ, FL, JS), pp. 170–184.
TACAS-2007-KatoenKZJ #bisimulation #model checking #probability: Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking (JPK, TK, ISZ, DNJ), pp. 87–101.
TACAS-2007-KupferschmidDHFDPB #heuristic #model checking: Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking (SK, KD, JH, BF, HD, AP, GB), pp. 679–682.
TACAS-2007-ManoliosOV #consistency: Checking Pedigree Consistency with PCS (PM, MGO, SOV), pp. 339–342.
TACAS-2007-YuCL #bound #diagrams #reachability #using: Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams (AJY, GC, GL), pp. 648–663.
PLDI-2007-BurckhardtAM #concurrent #consistency #data type #memory management #modelling #named: CheckFence: checking consistency of concurrent data types on relaxed memory models (SB, RA, MMKM), pp. 12–21.
PLDI-2007-ShankarB #automation #data type #invariant #java #named: DITTO: automatic incrementalization of data structure invariant checks (in Java) (AS, RB), pp. 310–319.
SAS-2007-CalcagnoPV #composition #concurrent #fine-grained #safety: Modular Safety Checking for Fine-Grained Concurrency (CC, MJP, VV), pp. 233–248.
CIAA-2007-Vardi #automaton #linear #model checking: Linear-Time Model Checking: Automata Theory in Practice (MYV), pp. 5–10.
ICALP-2007-ChuKM #correctness: Checking and Spot-Checking the Correctness of Priority Queues (MC, SK, AM), pp. 728–739.
ICALP-2007-TorreP #complexity #model checking #on the #recursion #state machine: On the Complexity of LtlModel-Checking of Recursive State Machines (SLT, GP), pp. 937–948.
LATA-2007-TabakovV #model checking #specification: Model Checking Buechi Specifications (DT, MYV), pp. 565–576.
SEFM-2007-PernaG #model checking #specification: Model Checking RAISE Applicative Specifications (JIP, CG), pp. 257–268.
SEFM-2007-RungtaM #benchmark #metric #model checking: Hardness for Explicit State Software Model Checking Benchmarks (NR, EGM), pp. 247–256.
SFM-2007-KwiatkowskaNP #model checking #probability: Stochastic Model Checking (MZK, GN, DP), pp. 220–270.
IFL-2007-FindlerGR #contract #data type #lazy evaluation: Lazy Contract Checking for Immutable Data Structures (RBF, SyG, AR), pp. 111–128.
IFL-2007-Kleeblatt #dependent type #using: Checking Dependent Types Using Compiled Code (DK), pp. 165–182.
IFL-2007-LiT #erlang #quickcheck #refactoring #testing: Testing Erlang Refactorings with QuickCheck (HL, SJT), pp. 19–36.
AGTIVE-2007-AmelunxenLSS #graph transformation #guidelines #modelling: Checking and Enforcement of Modeling Guidelines with Graph Transformations (CA, EL, AS, IS), pp. 313–328.
EDOC-2007-HalleVCG #model checking #workflow: Model Checking Data-Aware Workflow Properties with CTL-FO+ (SH, RV, OC, BG), pp. 267–278.
ICEIS-EIS-2007-MoralesTA #behaviour #consistency #modelling #semantics #uml: Checking Behavioural Consistency of UML-RT Models through Trace-Based Semantics (LEMM, MICT, KBA), pp. 205–211.
ICEIS-J-2007-CardosoABSS #integration: Inter-enterprise System and Application Integration: A Reality Check (JC, WMPvdA, CB, APS, KS), pp. 3–15.
MoDELS-2007-XuL #interactive #monitoring #visual notation: Formally Defining a Graphical Language for Monitoring and Checking Object Interactions (KX, DL), pp. 620–634.
MoDELS-2007-XuL #interactive #monitoring #visual notation: Formally Defining a Graphical Language for Monitoring and Checking Object Interactions (KX, DL), pp. 620–634.
OOPSLA-2007-BierhoffA #alias #composition #type system: Modular typestate checking of aliased objects (KB, JA), pp. 301–320.
TOOLS-EUROPE-2007-EkmanH #java: Pluggable checking and inferencing of nonnull types for Java (TE, GH), pp. 455–475.
PPDP-2007-CheneyM #model checking: Mechanized metatheory model-checking (JC, AM), pp. 75–86.
PADL-2007-Hughes #quickcheck #testing: QuickCheck Testing for Fun and Profit (JH), pp. 1–32.
PADL-2007-PodelskiR #abstraction #logic #model checking #named #refinement: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement (AP, AR), pp. 245–259.
RE-2007-SabetzadehNLEC #concept #consistency #model merging #modelling: Consistency Checking of Conceptual Models via Model Merging (MS, SN, SL, SME, MC), pp. 221–230.
SAC-2007-FerreiraLO #approach #java #model checking: A Java code annotation approach for model checking software systems (GF, EL, EASO), pp. 1536–1537.
SAC-2007-Kofron #behaviour #component #protocol #using: Checking software component behavior using behavior protocols and spin (JK), pp. 1513–1517.
SAC-2007-OliveiraAS #component #formal method #model checking #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.
ESEC-FSE-2007-FosterEKMRU #composition #constraints #model checking: Model checking service compositions under resource constraints (HF, WE, JK, JM, DSR, SU), pp. 225–234.
ESEC-FSE-2007-KosterK #behaviour #test coverage #testing: State coverage: a structural test adequacy criterion for behavior checking (KK, DCK), pp. 541–544.
ICSE-2007-Egyed07a #consistency #modelling #named #uml: UML/Analyzer: A Tool for the Instant Consistency Checking of UML Models (AE), pp. 793–796.
HPCA-2007-MeixnerS #detection #fault #online: Error Detection via Online Checking of Cache Coherence with Token Coherence Signatures (AM, DJS), pp. 145–156.
AMOST-2007-SatpathyR #abstraction #formal method #generative #model checking #modelling #refinement #testing: Test case generation from formal models through abstraction refinement and model checking (MS, SR), pp. 85–94.
AMOST-2007-WijesekeraASF #model checking #specification #testing: Relating counterexamples to test cases in CTL model checking specifications (DW, PA, LS, GF), pp. 75–84.
CADE-2007-BaeldeGMNT #model checking: The Bedwyr System for Model Checking over Syntactic Expressions (DB, AG, DM, GN, AT), pp. 391–397.
CADE-2007-GhilardiNRZ #infinity #model checking #satisfiability: Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems (SG, EN, SR, DZ), pp. 362–378.
CADE-2007-KuncakR #algebra #performance #satisfiability #towards: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic (VK, MCR), pp. 215–230.
CADE-2007-PerezV #bound #effectiveness #encoding #logic #ltl #model checking: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic (JANP, AV), pp. 346–361.
CAV-2007-BeyerHT #configuration management #convergence #model checking #program analysis #verification: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis (DB, TAH, GT), pp. 504–518.
CAV-2007-BrummayerB #c #named #satisfiability: C32SAT: Checking C Expressions (RB, AB), pp. 294–297.
CAV-2007-CharltonH #analysis #model checking #named #plugin: Hector: Software Model Checking with Cooperating Analysis Plugins (NC, MH), pp. 168–172.
CAV-2007-JonssonS #model checking: Systematic Acceleration in Regular Model Checking (BJ, MS), pp. 131–144.
CAV-2007-MatsliahS #approximate #encryption #model checking #random: Underapproximation for Model-Checking Based on Random Cryptographic Constructions (AM, OS), pp. 339–351.
CAV-2007-Segelken #abstraction #automaton #hybrid #linear #model checking #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: Model-Checking First-Order Logic: Automata and Locality (AD), p. 6.
ISSTA-2007-HughesB #composition #interface #model checking: Interface grammars for modular software model checking (GH, TB), pp. 39–49.
LICS-2007-KahlerKT #encryption #infinity #model checking #protocol: Infinite State AMC-Model Checking for Cryptographic Protocols (DK, RK, TT), pp. 181–192.
MBT-2007-KollmannH #generative #multi: Generating Scenarios by Multi-Object Checking (MK, YMH), pp. 61–72.
RTA-2007-EscobarM #infinity #model checking #using: Symbolic Model Checking of Infinite-State Systems Using Narrowing (SE, JM), pp. 153–168.
TAP-2007-Gargantini #detection #fault #model checking #testing #using: Using Model Checking to Generate Fault Detecting Tests (AG), pp. 189–206.
TestCom-FATES-2007-GromovW #model checking #testing: Testing and Model-Checking Techniques for Diagnosis (MG, TACW), pp. 138–154.
VMCAI-2007-GulwaniT: Assertion Checking Unified (SG, AT), pp. 363–377.
VMCAI-2007-McMillan #model checking: Interpolants and Symbolic Model Checking (KLM), pp. 89–90.
VMCAI-2007-MightCS #model checking: Model Checking Via GammaCFA (MM, BC, OS), pp. 59–73.
VMCAI-2007-Siegel #model checking #source code: Model Checking Nonblocking MPI Programs (SFS), pp. 44–58.
VMCAI-2007-Vardi #formal method #model checking #revisited: Automata-Theoretic Model Checking Revisited (MYV), pp. 137–150.
CBSE-2006-LauU #component #contract #deployment: Defining and Checking Deployment Contracts for Software Components (KKL, VU), pp. 1–16.
ASE-2006-ArthoG #model checking: Accurate Centralization for Applying Model Checking on Networked Applications (CA, PLG), pp. 177–188.
ASE-2006-DengLR #bound #execution #named #symbolic computation: Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems (XD, JL, R), pp. 157–166.
ASE-2006-Rajamani #automation #past present future: Automatic Property Checking for Software: Past, Present and Future (SKR), p. 12.
ASE-2006-RobbyDH #framework #model checking #using: Domain-specific Model Checking Using The Bogor Framework (R, MBD, JH), pp. 369–370.
ASE-2006-Volanschi #approach: A Portable Compiler-Integrated Approach to Permanent Checking (ENV), pp. 103–112.
DAC-2006-AwedhS #automation #bound #invariant #model checking: Automatic invariant strengthening to prove properties in bounded model checking (MA, FS), pp. 1073–1076.
DAC-2006-ElbazTSGBM #encryption: A parallelized way to provide data encryption and integrity checking on a processor-memory bus (RE, LT, GS, PG, MB, AM), pp. 506–509.
DAC-2006-GeorgelinK #design #equivalence #towards: Towards a C++-based design methodology facilitating sequential equivalence checking (PG, VK), pp. 93–96.
DAC-2006-PeranandamNRWKR #bound #performance: Fast falsification based on symbolic bounded property checking (PMP, PKN, JR, RJW, TK, WR), pp. 1077–1082.
DAC-2006-WuH #bound #constraints #equivalence #mining: Mining global constraints for improving bounded sequential equivalence checking (WW, MSH), pp. 743–748.
DATE-2006-DasBDC #design #model checking #question #what: What lies between design intent coverage and model checking? (SD, PB, PD, PPC), pp. 1217–1222.
PODS-2006-MachanavajjhalaG #on the #performance #privacy: On the efficiency of checking perfect privacy (AM, JG), pp. 163–172.
VLDB-2006-AfanasievFMZ #benchmark #framework #metric #named #xquery: XCheck: A Platform for Benchmarking XQuery Engines (LA, MF, MM, EZ), pp. 1247–1250.
ESOP-2006-GulwaniT #abstraction #linear: Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions (SG, AT), pp. 279–293.
TACAS-2006-LiS #abstraction #bound #model checking #performance #refinement: Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking (BL, FS), pp. 227–241.
TACAS-2006-NiebertP #ltl #model checking #partial order #performance: Efficient Model Checking for LTL with Partial Order Snapshots (PN, DP), pp. 272–286.
TACAS-2006-SenVA #markov #model checking #nondeterminism: Model-Checking Markov Chains in the Presence of Uncertainties (KS, MV, GA), pp. 394–410.
SCAM-J-2005-ZhangBCD06 #using: Using source transformation to test and model check implicit-invocation systems (HZ, JSB, JRC, JD), pp. 209–227.
CSMR-2006-MensK #source code: IntensiVE, a toolsuite for documenting and checking structural source-code regularities (KM, AK), pp. 239–248.
ICSM-2006-Hou #constraints #design #source code #using: Using Structural Constraints to Specify and Check Design Intent in Source Code — Ph.D. Dissertation Synopsis (DH), pp. 343–346.
PEPM-2006-LewisJ #analysis #model checking: A dead variable analysis for explicit model checking (ML, MJ), pp. 48–57.
SAS-2006-BouajjaniHRV #data type #model checking: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures (AB, PH, AR, TV), pp. 52–70.
FLOPS-2006-Tozawa #transducer #type checking #using #xml: XML Type Checking Using High-Level Tree Transducer (AT), pp. 81–96.
CIAA-2006-RoyC #finite #infinity #model checking: A Finite Union of DFAs in Symbolic Model Checking of Infinite Systems (SR, BC), pp. 277–278.
FM-2006-DonaldsonM #approximate #model checking #reduction #symmetry: Exact and Approximate Strategies for Symmetry Reduction in Model Checking (AFD, AM), pp. 541–556.
FM-2006-GenonMM #algorithm #distributed #ltl #monitoring #performance #sequence: Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces (AG, TM, CM), pp. 557–572.
FM-2006-JohnstonWBSR #model checking #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 #model checking #probability #refinement: Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems (AM), pp. 131–146.
FM-2006-PnueliZ #model checking #runtime #verification: PSL Model Checking and Run-Time Verification Via Testers (AP, AZ), pp. 573–586.
FM-2006-SchellhornGHR #challenge #proving: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse (GS, HG, DH, WR), pp. 16–31.
SEFM-2006-Rajamani #automation #past present future: Automatic Property Checking for Software: Past, Present and Future (SKR), pp. 18–20.
EDOC-2006-GovernatoriMS #contract #process: Compliance checking between business processes and business contracts (GG, ZM, SWS), pp. 221–232.
CIKM-2006-TheodoratosSDPS #graph #heuristic #query: Heuristic containment check of partial tree-pattern queries in the presence of index graphs (DT, SS, TD, PP, TKS), pp. 445–454.
SEKE-2006-Sarna-StarostaSD #approach #concurrent #modelling #multi #thread: A Model-based Design-for-Verification Approach to Checking for Deadlock in Multi-threaded Applications (BSS, REKS, LKD), pp. 120–125.
ECMDA-FA-2006-MesingCL #aspect-oriented #constraints #named: Limes: An Aspect-Oriented Constraint Checking Language (BM, CC, WL), pp. 299–315.
ECOOP-2006-Xie #automation #testing: Augmenting Automatically Generated Unit-Test Suites with Regression Oracle Checking (TX), pp. 380–403.
OOPSLA-2006-DargaB #data type #model checking #performance: Efficient software model checking of data structure properties (PTD, CB), pp. 363–382.
PPDP-2006-Volanschi #compilation #confluence #named: Condate: a proto-language at the confluence between checking and compiling (ENV), pp. 225–236.
POPL-2006-Flanagan #hybrid #type checking: Hybrid type checking (CF), pp. 245–256.
SAC-2006-EliasEC #consistency #multi: Dynamic consistency checking for temporal and spatial relations in multimedia presentations (SE, KSE, RC), pp. 1380–1384.
SAC-2006-JaghooriMS #model checking #named: Modere: the model-checking engine of Rebeca (MMJ, AM, MS), pp. 1810–1815.
SAC-2006-Sridhar #component: Dynamic instantiation-checking components (NS), pp. 1442–1446.
FSE-2006-GulavaniHKNR #algorithm #named: SYNERGY: a new algorithm for property checking (BSG, TAH, YK, AVN, SKR), pp. 117–127.
ICSE-2006-ChangJ #declarative #model checking #modelling #relational: Symbolic model checking of declarative relational models (FSHC, DJ), pp. 312–320.
ICSE-2006-DhurjatiA #array #bound #c: Backwards-compatible array bounds checking for C with very low overhead (DD, VSA), pp. 162–171.
ICSE-2006-DongHZQ #modelling #named: HighSpec: a tool for building and checking OZTA models (JSD, PH, XZ, SQ), pp. 775–778.
ICSE-2006-Egyed #consistency #uml: Instant consistency checking for the UML (AE), pp. 381–390.
ICSE-2006-HackettDWY #composition #in the large: Modular checking for buffer overflows in the large (BH, MD, DW, ZY), pp. 232–241.
ICSE-2006-XuCC #consistency #incremental #pervasive: Incremental consistency checking for pervasive context (CX, SCC, WKC), pp. 292–301.
CC-2006-LamprechtMS #analysis #data flow #model checking: Data-Flow Analysis as Model Checking Within the jABC (ALL, TMS, BS), pp. 101–104.
CAV-2006-BurckhardtAM #bound #case study #concurrent #data type #memory management #model checking #modelling: Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study (SB, RA, MMKM), pp. 489–502.
CAV-2006-HeljankoJKLL #automaton #bound #model checking: Bounded Model Checking for Weak Alternating Büchi Automata (KH, TAJ, MK, ML, TL), pp. 95–108.
CAV-2006-KahlonGS #concurrent #model checking #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-KloseTWW #performance #sequence chart #verification: Check It Out: On the Efficient Formal Verification of Live Sequence Charts (JK, TT, BW, HW), pp. 219–233.
CAV-2006-KwiatkowskaNP #model checking #probability #reduction #symmetry: Symmetry Reduction for Probabilistic Model Checking (MZK, GN, DP), pp. 234–248.
CAV-2006-LalR #automaton #model checking: Improving Pushdown System Model Checking (AL, TWR), pp. 343–357.
CAV-2006-SenA #model checking #testing #tool support: CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools (KS, GA), pp. 419–423.
CAV-2006-SenV #model checking #parallel #source code #thread: Model Checking Multithreaded Programs with Asynchronous Atomic Methods (KS, MV), pp. 300–314.
CAV-2006-WulfDHR #algorithm #anti #automaton #finite #named: Antichains: A New Algorithm for Checking Universality of Finite Automata (MDW, LD, TAH, JFR), pp. 17–30.
CSL-2006-GollerL #infinity #logic #model checking: Infinite State Model-Checking of Propositional Dynamic Logics (SG, ML), pp. 349–364.
CSL-2006-Kaiser #automation #game studies #model checking #quantifier: Game Quantification on Automatic Structures and Hierarchical Model Checking Games (LK), pp. 411–425.
FATES-RV-2006-ErnitsKRV #generative #model checking #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 #model checking #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 #model checking #thread: An Automata-Theoretic Approach for Model Checking Threads for LTL Propert (VK, AG), pp. 101–110.
LICS-2006-Ong #higher-order #model checking #on the #recursion: On Model-Checking Trees Generated by Higher-Order Recursion Schemes (CHLO), pp. 81–90.
LICS-2006-VaraccaV #logic #model checking: Temporal Logics and Model Checking for Fairly Correct Systems (DV, HV), pp. 389–398.
RTA-2006-Obua #higher-order #logic: Checking Conservativity of Overloaded Definitions in Higher-Order Logic (SO), pp. 212–226.
SAT-2006-JainBC #satisfiability #using: Satisfiability Checking of Non-clausal Formulas Using General Matings (HJ, CB, EMC), pp. 75–89.
TestCom-2006-ShuL #monitoring #protocol #security #testing: Message Confidentiality Testing of Security Protocols — Passive Monitoring and Active Checking (GS, DL), pp. 357–372.
TestCom-2006-UralZ #sequence: Reducing the Lengths of Checking Sequences by Overlapping (HU, FZ), pp. 274–288.
TestCom-2006-YalcinY #sequence #using: Using Distinguishing and UIO Sequences Together in a Checking Sequence (MCY, HY), pp. 259–273.
VMCAI-2006-Bozzelli #automaton #complexity #model checking: Complexity Results on Branching-Time Pushdown Model Checking (LB), pp. 65–79.
VMCAI-2006-GurfinkelWC #abstraction #model checking: Systematic Construction of Abstractions for Model-Checking (AG, OW, MC), pp. 381–397.
VMCAI-2006-HristovaL #algorithm #automaton #linear #logic #model checking: Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems (KH, YAL), pp. 190–206.
VMCAI-2006-JabbarE #linear #model checking #parallel: Parallel External Directed Model Checking with Linear I/O (SJ, SE), pp. 237–251.
VMCAI-2006-Younes #fault #model checking #probability: Error Control for Probabilistic Model Checking (HLSY), pp. 142–156.
WICSA-2005-MuskensBC #consistency: Generalizing Consistency Checking between Software Views (JM, RJB, MRVC), pp. 169–180.
ASE-2005-AgarwalSWS #concurrent #detection #runtime #using: Optimized run-time race detection and atomicity checking using partial discovered types (RA, AS, LW, SDS), pp. 233–242.
ASE-2005-DenmatDR #data mining #execution #mining: Data mining and cross-checking of execution traces: a re-interpretation of Jones, Harrold and Stasko test information (TD, MD, OR), pp. 396–399.
ASE-2005-HaydarBPS #model checking #web: Properties and scopes in web model checking (MH, SB, AP, HAS), pp. 400–404.
ASE-2005-RungtaM #heuristic #model checking: A context-sensitive structural heuristic for guided search model checking (NR, EGM), pp. 410–413.
ASE-2005-SimmondsB #automation #consistency #uml: A tool for automatic UML model consistency checking (JS, MCB), pp. 431–432.
ASE-2005-ZhangC #performance #query: Efficient temporal-logic query checking for presburger systems (DZ, RC), pp. 24–33.
DAC-2005-GanaiGA #model checking #safety #satisfiability: Beyond safety: customized SAT-based model checking (MKG, AG, PA), pp. 738–743.
DAC-2005-GeilenBS #data flow #graph #model checking #requirements: Minimising buffer requirements of synchronous dataflow graphs with model checking (MG, TB, SS), pp. 819–824.
DATE-2005-BolchiniSSP #reliability #self #specification: Reliable System Specification for Self-Checking Data-Paths (CB, FS, DS, LP), pp. 1278–1283.
DATE-2005-CabodiCNQ #bound #model checking #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 #model checking: Space-Efficient Bounded Model Checking (JK, ZH, ND), pp. 686–687.
DATE-2005-ShashidharBCJ #algebra #equivalence #functional #source code #verification: Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code (KCS, MB, FC, GJ), pp. 1310–1315.
DATE-2005-WenzelRKP #clustering #context-free grammar #generative #model checking: utomatic Timing Model Generation by CFG Partitioning and Model Checking (IW, BR, RK, PPP), pp. 606–611.
PODS-2005-ManethBPS #metaprogramming #transducer #type checking #xml: XML type checking with macro tree transducers (SM, AB, TP, HS), pp. 283–294.
VLDB-2005-YaoWJ: Checking for k-Anonymity Violation by Views (CY, XSW, SJ), pp. 910–921.
WRLA-2004-LiquoriW05 #calculus #polymorphism #type checking #type inference: The Polymorphic Rewriting-calculus: [Type Checking vs. Type Inference] (LL, BW), pp. 89–111.
WRLA-2004-Wang05 #calculus #maude #model checking #μ-calculus: μ-Calculus Model Checking in Maude (BYW), pp. 135–152.
ESOP-2005-ChanderEILN #bound #dynamic analysis #verification: Enforcing Resource Bounds via Static Verification of Dynamic Checks (AC, DE, NI, PL, GCN), pp. 311–325.
FASE-2005-BeyerHJM #memory management #safety: Checking Memory Safety with Blast (DB, TAH, RJ, RM), pp. 2–18.
FASE-2005-EichbergSM #using: Using Annotations to Check Structural Properties of Classes (ME, TS, MM), pp. 237–252.
FoSSaCS-2005-FerrariMT #calculus #model checking: Model Checking for Nominal Calculi (GLF, UM, ET), pp. 1–24.
FoSSaCS-2005-LaroussinieS #model checking #probability: Model Checking Durational Probabilistic Systems (FL, JS), pp. 140–154.
TACAS-2005-BaoJ #model checking: Time-Efficient Model Checking with Magnetic Disk (TB, MDJ), pp. 526–540.
TACAS-2005-BergaminiDJM #bisimulation #composition #equivalence #named #on the fly: BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking (DB, ND, CJ, RM), pp. 581–585.
TACAS-2005-BouajjaniHMV #model checking #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 #model checking #named #satisfiability #scalability #verification: DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems (MKG, AG, PA), pp. 575–580.
TACAS-2005-GrosuS #model checking #monte carlo: Monte Carlo Model Checking (RG, SAS), pp. 271–286.
TACAS-2005-HammerKM #ltl #model checking #on the fly: Truly On-the-Fly LTL Model Checking (MH, AK, SM), pp. 191–205.
TACAS-2005-KellerSBS #c #debugging #model checking #named #source code: FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs (CWK, DS, SB, SAS), pp. 563–569.
TACAS-2005-McMillan #model checking: Applications of Craig Interpolants in Model Checking (KLM), pp. 1–12.
TACAS-2005-QadeerR #bound #concurrent #model checking: Context-Bounded Model Checking of Concurrent Software (SQ, JR), pp. 93–107.
TACAS-2005-RemkeHC #infinity #markov #model checking: Model Checking Infinite-State Markov Chains (AR, BRH, LC), pp. 237–252.
TACAS-2005-SchuppanB #ltl #model checking: Shortest Counterexamples for Symbolic Model Checking of LTL with Past (VS, AB), pp. 493–509.
TACAS-2005-SharmaPC #bound #logic: Bounded Validity Checking of Interval Duration Logic (BS, PKP, SC), pp. 301–316.
IWPC-2005-Reiss #java #specification #tool support: Tool Demonstration: CHET: Checking Specifications in Java Systems (SPR), pp. 165–168.
SCAM-2005-HongLS #abstract interpretation #approach #model checking #slicing: Abstract Slicing: A New Approach to Program Slicing Based on Abstract Interpretation and Model Checking (HSH, IL, OS), pp. 25–34.
PLDI-2005-FurrF #type safety: Checking type safety of foreign function calls (MF, JSF), pp. 62–72.
CIAA-2005-SudaH #algorithm #automaton #backtracking #top-down: Non-backtracking Top-Down Algorithm for Checking Tree Automata Containment (TS, HH), pp. 294–306.
FM-2005-DonaldsonM #automation #detection #model checking #symmetry #using: Automatic Symmetry Detection for Model Checking Using Computational Group Theory (AFD, AM), pp. 481–496.
FM-2005-EislerSJSS #case study #model checking: Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications (SE, CS, BJ, GS, JS), pp. 533–536.
FM-2005-HoenickeM #model checking #process #specification: Model-Checking of Specifications Integrating Processes, Data and Time (JH, PM), pp. 465–480.
FM-2005-IyerSEJ #clustering #model checking #on the: On Partitioning and Symbolic Model Checking (SKI, DS, EAE, JJ), pp. 497–511.
FM-2005-WoodcockCF #model checking #semantics: Operational Semantics for Model Checking Circus (JW, AC, LF), pp. 237–252.
IFM-2005-GodefroidK #model checking: Software Model Checking: Searching for Computations in the Abstract or the Concrete (PG, NK), pp. 20–32.
IFM-2005-LamP #consistency #diagrams #sequence chart #statechart #using #π-calculus: Consistency Checking of Sequence Diagrams and Statechart Diagrams Using the π-Calculus (VSWL, JAP), pp. 347–365.
SEFM-2005-CeroneLC #analysis #formal method #human-computer #interactive #model checking #using: Formal Analysis of Human-computer Interaction using Model-checking (AC, PAL, SC), pp. 352–362.
CIKM-2005-HaradaH #order #using: Order checking in a CPOE using event analyzer (LH, YH), pp. 549–555.
CIKM-2005-RotemSW #optimisation: Optimizing candidate check costs for bitmap indices (DR, KS, KW), pp. 648–655.
SEKE-2005-IzadiM #algorithm #calculus #model checking #performance #μ-calculus: An Efficient Model Checking Algorithm for a Fragment of μ-Calculus (MI, AMR), pp. 392–395.
ECOOP-2005-LamP #consistency #diagrams #statechart: Consistency Checking of Statechart Diagrams of a Class Hierarchy (VSWL, JAP), pp. 412–427.
OOPSLA-2005-DoorenS #exception #flexibility #robust #using: Combining the robustness of checked exceptions with the flexibility of unchecked exceptions using anchored exception declarations (MvD, ES), pp. 455–471.
QAPL-2004-AlpuenteGPV05 #model checking #source code: Abstract Model Checking of tccp programs (MA, MdMG, EP, AV), pp. 19–36.
PADL-2005-YangDRS #compilation #mobile #model checking #performance #process: A Provably Correct Compiler for Efficient Model Checking of Mobile Processes (PY, YD, CRR, SAS), pp. 113–127.
POPL-2005-FlanaganG #model checking #partial order #reduction: Dynamic partial-order reduction for model checking software (CF, PG), pp. 110–121.
SAC-2005-Arias-FisteusFK #model checking: Applying model checking to BPEL4WS business collaborations (JAF, LSF, CDK), pp. 826–830.
ICSE-2005-CsallnerS #static analysis #testing: Check’n’crash: combining static checking and testing (CC, YS), pp. 422–431.
ICSE-2005-McClureK #sql: SQL DOM: compile time checking of dynamic SQL statements (RAM, IHK), pp. 88–96.
CC-2005-ShashidharBCJ #equivalence #program transformation #source code #verification: Verification of Source Code Transformations by Program Equivalence Checking (KCS, MB, FC, GJ), pp. 221–236.
PPoPP-2005-ShachamSS #information management #model checking #scalability #using: Scaling model checking of dataraces using dynamic information (OS, MS, AS), pp. 107–118.
CAV-2005-BalakrishnanRKLLMGYCT #bytecode #model checking: 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 #model checking #using: Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework (MBD, JH, MH, R), pp. 148–152.
CAV-2005-GeeraertsRB #performance: Expand, Enlarge and Check... Made Efficient (GG, JFR, LVB), pp. 394–407.
CAV-2005-GuptaS #abstraction #bound #model checking #refinement: Abstraction Refinement for Bounded Model Checking (AG, OS), pp. 112–124.
CAV-2005-HeljankoJL #bound #incremental #model checking: Incremental and Complete Bounded Model Checking for Full PLTL (KH, TAJ, TL), pp. 98–111.
CAV-2005-PasareanuPV #model checking #refinement: Concrete Model Checking with Abstract Matching and Refinement (CSP, RP, WV), pp. 52–66.
CAV-2005-PiazzaAMPWM #algebra #algorithm #biology #challenge #model checking: Algorithmic Algebraic Model Checking I: Challenges from Systems Biology (CP, MA, VM, AP, FW, BM), pp. 5–19.
CAV-2005-RabinovitzG #bound #concurrent #model checking #source code: Bounded Model Checking of Concurrent Programs (IR, OG), pp. 82–97.
CAV-2005-SebastianiTV #hybrid #ltl #model checking: Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking (RS, ST, MYV), pp. 350–363.
CAV-2005-SenVA #model checking #on the #probability #statistics: On Statistical Model Checking of Stochastic Systems (KS, MV, GA), pp. 266–280.
CAV-2005-TangMGI #model checking #reduction #satisfiability #symmetry: Symmetry Reduction in SAT-Based Model Checking (DT, SM, AG, CNI), pp. 125–138.
CSL-2005-Blanqui #algebra #calculus #decidability: Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations (FB), pp. 135–150.
CSL-2005-CharatonikGM #bound #model checking #pointer #source code: Bounded Model Checking of Pointer Programs (WC, LG, PM), pp. 397–412.
FATES-2005-PetrenkoY #automaton #consistency #nondeterminism #testing: Conformance Tests as Checking Experiments for Partial Nondeterministic FSM (AP, NY), pp. 118–133.
ICLP-2005-Mallya #deduction #model checking #multi: Deductive Multi-valued Model Checking (AM), pp. 297–310.
ICLP-2005-TompitsW #equivalence #implementation #programming #towards: Towards Implementations for Advanced Equivalence Checking in Answer-Set Programming (HT, SW), pp. 189–203.
LICS-2005-GodefroidH #logic #model checking #semantics: Model Checking Vs. Generalized Model Checking: Semantic Minimizations for Temporal Logics (PG, MH), pp. 158–167.
LICS-2005-Lohrey #model checking: Model-Checking Hierarchical Structures (ML), pp. 168–177.
SAT-2005-DershowitzHK #bound #model checking: Bounded Model Checking with QBF (ND, ZH, JK), pp. 408–414.
SAT-2005-Goldberg #equivalence #specification: Equivalence Checking of Circuits with Parameterized Specifications (EG), pp. 107–121.
SAT-2005-Zarpas #benchmark #bound #metric #model checking #satisfiability: Benchmarking SAT Solvers for Bounded Model Checking (EZ), pp. 340–354.
TestCom-2005-ChenHUY #sequence #testing: Eliminating Redundant Tests in a Checking Sequence (JC, RMH, HU, HY), pp. 146–158.
TestCom-2005-LadaniAC #approach #invariant #testing: Passive Testing — A Constrained Invariant Checking Approach (BTL, BA, ARC), pp. 9–22.
VMCAI-2005-AbrahamBKS #bound #hybrid #linear #model checking #optimisation: Optimizing Bounded Model Checking for Linear Hybrid Systems (EÁ, BB, FK, MS), pp. 396–412.
VMCAI-2005-Bozzelli #model checking #process #term rewriting: Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties (LB), pp. 282–297.
VMCAI-2005-JabbarE #model checking #performance: I/O Efficient Directed Model Checking (SJ, SE), pp. 313–329.
VMCAI-2005-LamKR #consistency #data type #type system: Generalized Typestate Checking for Data Structure Consistency (PL, VK, MCR), pp. 430–447.
VMCAI-2005-LatvalaBHJ #bound #ltl #model checking #performance: Simple Is Better: Efficient Bounded Model Checking for Past LTL (TL, AB, KH, TAJ), pp. 380–395.
VMCAI-2005-Muller-OlmRS: Checking Herbrand Equalities and Beyond (MMO, OR, HS), pp. 79–96.
VMCAI-2005-SistlaZW #commutative #model checking: Model Checking of Systems Employing Commutative Functions (APS, MZ, XW), pp. 250–266.
ASE-2004-Andrews #case study #data type #random #testing: Case Study of Coverage-Checked Random Data Structure Testing (JHA), pp. 316–319.
ASE-2004-ChoiH #approach #case study #model checking: Combination Model Checking: Approach and a Case Study (YC, MPEH), pp. 354–357.
ASE-2004-DwyerRTV #interactive #model checking #order: Analyzing Interaction Orderings with Model Checking (MBD, R, OT, WV), pp. 154–163.
ASE-2004-RauschmayerKW #consistency #framework #generative #scalability: Consistency Checking in an Infrastructure for Large-Scale Generative (AR, AK, MW), pp. 238–247.
ASE-2004-Reiss #named #specification: CHET: A System for Checking Dynamic Specifications (SPR), pp. 302–305.
DAC-2004-AnastasakisMP #equivalence #performance: Efficient equivalence checking with partitions and hierarchical cut-points (DA, LM, SP), pp. 539–542.
DAC-2004-MohiyuddinPAW: Synthesizing interconnect-efficient low density parity check codes (MM, AP, AA, WW), pp. 488–491.
DAC-2004-WangJHS #bound #model checking #satisfiability: Refining the SAT decision ordering for bounded model checking (CW, HJ, GDH, FS), pp. 535–538.
DATE-DF-2004-KruppMO #model checking #refinement: Formal Refinement and Model Checking of an Echo Cancellation Unit (AK, WM, IO), pp. 102–107.
DATE-v2-2004-NardiS #synthesis: Synthesis for Manufacturability: A Sanity Check (AN, ALSV), pp. 796–803.
DATE-v2-2004-SogomonyanMOG #self: A New Self-Checking Sum-Bit Duplicated Carry-Select Adder (ESS, DM, VO, MG), pp. 1360–1361.
DATE-2005-UmezawaS04 #verification: A Formal Verification Methodology for Checking Data Integrity (YU, TS), pp. 284–289.
FASE-2004-HuismanGSC #case study #interactive: Checking Absence of Illicit Applet Interactions: A Case Study (MH, DG, CS, GC), pp. 84–98.
FASE-2004-SaffreyC #communication #model checking #optimisation: Optimising Communication Structure for Model Checking (PS, MC), pp. 310–323.
FASE-2004-XieLKB #design #model checking: Translating Software Designs for Model Checking (FX, VL, RPK, JCB), pp. 324–338.
TACAS-2004-AlfaroFHMS #model checking: Model Checking Discounted Temporal Properties (LdA, MF, TAH, RM, MS), pp. 77–92.
TACAS-2004-BoigelotLW #model checking: ω-Regular Model Checking (BB, AL, PW), pp. 561–575.
TACAS-2004-ClarkeKL #source code: A Tool for Checking ANSI-C Programs (EMC, DK, FL), pp. 168–176.
TACAS-2004-Muller-OlmY #animation #game studies #model checking #named: MetaGame: An Animation Tool for Model-Checking Games (MMO, HY), pp. 163–167.
TACAS-2004-QianN #abstraction #database #invariant #model checking: Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases (KQ, AN), pp. 497–511.
TACAS-2004-RaviS #bound #model checking: Minimal Assignments for Bounded Model Checking (KR, FS), pp. 31–45.
TACAS-2004-RobbyRDH #framework #model checking #specification #using: Checking Strong Specifications Using an Extensible Software Model Checking Framework (R, ER, MBD, JH), pp. 404–420.
TACAS-2004-YounesKNP #empirical #model checking #probability #statistics: Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study (HLSY, MZK, GN, DP), pp. 46–60.
ICSM-2004-XieN #black box #difference #testing: Checking Inside the Black Box: Regression Testing Based on Value Spectra Differences (TX, DN), pp. 28–37.
IWPC-2004-BeyerHJM #eclipse #model checking #plugin: An Eclipse Plug-in for Model Checking (DB, TAH, RJ, RM), pp. 251–255.
PASTE-2004-Godefroid #model checking: Invited Talk: “Model checking” software with VeriSoft (PG), p. 36.
PLDI-2004-HenzingerJM: Race checking by context inference (TAH, RJ, RM), pp. 1–13.
PLDI-2004-VenetB #array #bound #c #embedded #performance #precise #scalability #source code: Precise and efficient static array bound checking for large embedded C programs (AV, GPB), pp. 231–242.
CIAA-2004-ZakharovZ #automaton #multi #on the #problem #source code: On the Equivalence-Checking Problem for a Model of Programs Related with Multi-tape Automata (VAZ, IZ), pp. 293–305.
ICALP-2004-BrunsG #logic #model checking #multi: Model Checking with Multi-valued Logics (GB, PG), pp. 281–293.
IFM-2004-ChakiCOSS #model checking: State/Event-Based Software Model Checking (SC, EMC, JO, NS, NS), pp. 128–147.
IFM-2004-Melham #functional #model checking #proving #theorem proving: Integrating Model Checking and Theorem Proving in a Reflective Functional Language (TFM), pp. 36–39.
IFM-2004-WangRL #csp #independence #reachability: Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption (XW, AWR, RL), pp. 247–266.
SEFM-2004-SchuleS #comparison #infinity #model checking #verification: Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems (TS, KS), pp. 67–76.
SEFM-2004-SistlaWZ #using: Checking Extended CTL properties Using Guarded Quotient Structures (APS, XW, MZ), pp. 87–94.
ICGT-2004-RensinkSV #comparison #graph transformation #model checking: Model Checking Graph Transformations: A Comparison of Two Approaches (AR, ÁS, DV), pp. 226–241.
ICEIS-v1-2004-Augusto #model checking #theorem proving #verification: Model Checking and Theorem Proving-Based Verification of EIS (JCA), p. XXXIII-XXXIV.
ICEIS-v3-2004-StantonM #design #model checking #object-oriented: Model Checking an Object-Oriented Design (SCS, VMM), pp. 605–608.
ICPR-v2-2004-TangASBC #recognition: Recognition of Unconstrained Legal Amounts Handwritten on Chinese Bank Checks (HT, EA, CYS, OB, MC), pp. 610–613.
KR-2004-EiterFFPW #bound #complexity #model checking #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 #model checking #petri net #prolog: Model checking object petri nets in prolog (BF, ML), pp. 20–31.
SAC-J-2003-Paradkar04 #consistency #generative #interactive #modelling #self #testing #towards: Towards model-based generation of self-priming and self-checking conformance tests for interactive system (AMP), pp. 315–322.
SAC-2004-MadirajuS #approach #constraints #database #mobile: A mobile agent approach for global database constraint checking (PM, RS), pp. 679–683.
ICSE-2004-GouldSD #database #query #static analysis: Static Checking of Dynamically Generated Queries in Database Applications (CG, ZS, PTD), pp. 645–654.
LDTA-2004-GradaraSVV #model checking #modelling #parallel #source code #thread: Model Checking Multithreaded Programs by Means of Reduced Models (SG, AS, MLV, GV), pp. 55–74.
OSDI-2004-YangTEM #exclamation #fault #file system #model checking #using: Using Model Checking to Find Serious File System Errors (Awarded Best Paper!) (JY, PT, DRE, MM), pp. 273–288.
CAV-2004-AbdullaJNdS #ltl #model checking: Regular Model Checking for LTL(MSO) (PAA, BJ, MN, Jd, MS), pp. 348–360.
CAV-2004-AwedhS #bound #model checking #proving: Proving More Properties with Bounded Model Checking (MA, FS), pp. 96–108.
CAV-2004-BouajjaniHV #model checking: Abstract Regular Model Checking (AB, PH, TV), pp. 372–386.
CAV-2004-FinkelL #image #infinity #model checking: Image Computation in Infinite State Model Checking (AF, JL), pp. 361–371.
CAV-2004-GammieM #logic #model checking #named: MCK: Model Checking the Logic of Knowledge (PG, RvdM), pp. 479–483.
CAV-2004-GanaiGA #bound #embedded #model checking #modelling #performance: Efficient Modeling of Embedded Memories in Bounded Model Checking (MKG, AG, PA), pp. 440–452.
CAV-2004-GoelB #abstraction #functional #model checking #order #simulation: Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors (AG, REB), pp. 255–267.
CAV-2004-JinAS #bound #model checking #named #satisfiability #towards: CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking (HJ, MA, FS), pp. 519–522.
CAV-2004-Lange #model checking: Symbolic Model Checking of Non-regular Properties (ML), pp. 83–95.
CAV-2004-Metzner #analysis #model checking #why: Why Model Checking Can Improve WCET Analysis (AM), pp. 334–347.
CAV-2004-Namjoshi #model checking: An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking (KSN), pp. 57–69.
CAV-2004-PitermanV #infinity #model checking: Global Model-Checking of Infinite-State Systems (NP, MYV), pp. 387–400.
CAV-2004-SchroterK #model checking #parallel #petri net: Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings (CS, VK), pp. 109–121.
CAV-2004-SebastianiSTV #model checking: GSTE Is Partitioned Model Checking (RS, ES, ST, MYV), pp. 229–241.
CAV-2004-SenVA #black box #model checking #probability #statistics: Statistical Model Checking of Black-Box Probabilistic Systems (KS, MV, GA), pp. 202–215.
CAV-2004-YangS #composition #model checking #specification: Compositional Specification and Model Checking in GSTE (JY, CJHS), pp. 216–228.
CSL-2004-EmersonK #message passing #model checking: Parameterized Model Checking of Ring-Based Message Passing Systems (EAE, VK), pp. 325–339.
CSL-2004-McMillan #model checking: Applications of Craig Interpolation to Model Checking (KLM), pp. 22–23.
FATES-2004-HongU #cost analysis #generative #model checking #testing #using: Using Model Checking for Reducing the Cost of Test Generation (HSH, HU), pp. 110–124.
FATES-2004-XieD #approach #component #model checking: An Automata-Theoretic Approach for Model-Checking Systems with Unspecified Components (GX, ZD), pp. 155–169.
IJCAR-2004-BartheCT #formal method #random: A Machine-Checked Formalization of the Generic Model and the Random Oracle Model (GB, JC, ST), pp. 385–399.
IJCAR-2004-RiazanovV #constraints #performance: Efficient Checking of Term Ordering Constraints (AR, AV), pp. 60–74.
LICS-2004-DamsN #abstraction #branch #finite #model checking: The Existence of Finite Abstractions for Branching Time Model Checking (DD, KSN), pp. 335–344.
LICS-2004-EsparzaKM #automaton #model checking #probability: Model Checking Probabilistic Pushdown Automata (JE, AK, RM), pp. 12–21.
LICS-2004-FlumG #model checking #problem: Model-Checking Problems as a Basis for Parameterized Intractability (JF, MG), pp. 388–397.
LICS-2004-WohrleT #infinity #model checking: Model Checking Synchronized Products of Infinite Transition Systems (SW, WT), pp. 2–11.
VMCAI-2004-ClarkeKOS #bound #complexity #model checking: Completeness and Complexity of Bounded Model Checking (EMC, DK, JO, OS), pp. 85–96.
VMCAI-2004-EnglerM #debugging #model checking #static analysis: Static Analysis versus Software Model Checking for Bug Finding (DRE, MM), pp. 191–210.
VMCAI-2004-HatcliffRD #concurrent #model checking #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 #model checking #probability: Approximate Probabilistic Model Checking (TH, RL, FM, SP), pp. 73–84.
VMCAI-2004-LucanuC #algebra #model checking #specification: Model Checking for Object Specifications in Hidden Algebra (DL, GC), pp. 97–109.
VMCAI-2004-PaceS #difference #kernel #model checking #using: Model Checking Polygonal Differential Inclusions Using Invariance Kernels (GJP, GS), pp. 110–121.
VMCAI-2004-YuX: Checking Interval Based Properties for Reactive Systems (YP, QX), pp. 122–134.
ASE-2003-BarnatBC #ltl #model checking #parallel: Parallel Breadth-First Search LTL Model-Checking (JB, LB, JC), pp. 106–115.
ASE-2003-ChoiH #abstraction #model checking #reduction #requirements #specification #using: Model Checking Software Requirement Specifications using Domain Reduction Abstraction (YC, MPEH), pp. 314–317.
ASE-2003-TkachukDP #automation #generative #model checking: Automated Environment Generation for Software Model Checking (OT, MBD, CSP), pp. 116–129.
ASE-2003-TurnerGWBHSR #consistency #constraints #diagrams #implementation #modelling #runtime #uml #visual notation: Visual Constraint Diagrams: Runtime Conformance Checking of UML Object Models versus Implementations (CJT, TCNG, CW, JB, DH, HDS, AGR), pp. 271–276.
DAC-2003-ClarkeKY #behaviour #bound #c #consistency #model checking #source code #using: Behavioral consistency of C and verilog programs using bounded model checking (EMC, DK, KY), pp. 368–371.
DAC-2003-DamianoK #satisfiability: Checking satisfiability of a conjunction of BDDs (RFD, JHK), pp. 818–823.
DAC-2003-GuptaGWYA #bound #learning #model checking #satisfiability: Learning from BDDs in SAT-based bounded model checking (AG, MKG, CW, ZY, PA), pp. 824–829.
DAC-2003-KangP #bound #model checking #satisfiability: SAT-based unbounded symbolic model checking (HJK, ICP), pp. 840–843.
DATE-2003-CabodiNQ #approximate #bound #model checking #satisfiability #traversal: Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals (GC, SN, SQ), pp. 10898–10905.
DATE-2003-OikonomakosZA #metric #online #self #synthesis #testing #using: Versatile High-Level Synthesis of Self-Checking Datapaths Using an On-Line Testability Metric (PO, MZ, BMAH), pp. 10596–10601.
DATE-2003-WedlerSK #encoding #induction #using: Using RTL Statespace Information and State Encoding for Induction Based Property Checking (MW, DS, WK), pp. 11156–11157.
ICDAR-2003-GrecoILSS: Bank-check Processing System: Modifications Due to the New European Currency (NG, DI, MGL, AS, LS), pp. 343–348.
VLDB-2003-KornMZ #database #monitoring #network #problem #quality: Checks and Balances: Monitoring Data Quality Problems in Network Traffic Databases (FK, SM, YZ), pp. 536–547.
ESOP-2003-Flanagan #automation #model checking #using: Automatic Software Model Checking Using CLP (CF), pp. 189–203.
FASE-2003-SharyginaB #abstraction #model checking: Model Checking Software via Abstraction of Loop Transitions (NS, JCB), pp. 325–340.
FoSSaCS-2003-BertrandS #decidability #model checking: Model Checking Lossy Channels Systems Is Probably Decidable (NB, PS), pp. 120–135.
TACAS-2003-AmlaKMM #analysis #bound #model checking: Experimental Analysis of Different Techniques for Bounded Model Checking (NA, RPK, KLM, RM), pp. 34–48.
TACAS-2003-BenedettiC #bound #ltl #model checking: Bounded Model Checking for Past LTL (MB, AC), pp. 18–33.
TACAS-2003-EmersonK #agile #model checking #protocol: Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols (EAE, VK), pp. 144–159.
TACAS-2003-KhurshidPV #execution #model checking #symbolic computation #testing: Generalized Symbolic Execution for Model Checking and Testing (SK, CSP, WV), pp. 553–568.
TACAS-2003-VaziriJ #constraints #theorem proving: Checking Properties of Heap-Manipulating Procedures with a Constraint Solver (MV, DJ), pp. 505–520.
CSMR-2003-SciascioDMP #design #maintenance #model checking #using #web: Web Applications Design and Maintenance Using Symbolic Model Checking (EDS, FMD, MM, GP), pp. 63–72.
SCAM-2003-MoseleyDA: Checking Program Profiles (PM, SKD, GRA), pp. 193–202.
PLDI-2003-AikenFKT #alias: Checking and inferring local non-aliasing (AA, JSF, JK, TT), pp. 129–140.
SAS-2003-Boyland: Checking Interference with Fractional Permissions (JB), pp. 55–72.
CIAA-2003-TozawaH #xml: XML Schema Containment Checking Based on Semi-implicit Techniques (AT, MH), pp. 213–225.
ICALP-2003-Peled #model checking #testing: Model Checking and Testing Combined (DP), pp. 47–63.
ICALP-2003-Schnoebelen #model checking: Oracle Circuits for Branching-Time Model Checking (PS), pp. 790–801.
FME-2003-ArmandoCG #analysis #graph #model checking #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 #model checking #validation: Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle (DC, PI, PP, AS), pp. 114–132.
FME-2003-DongSW #alloy #reasoning #semantics #web: Checking and Reasoning about Semantic Web through Alloy (JSD, JS, HHW), pp. 796–813.
FME-2003-Glesner: Program Checking with Certificates: Separating Correctness-Critical Code (SG), pp. 758–777.
FME-2003-GoldsmithMRWZ #model checking: Watchdog Transformations for Property-Oriented Model-Checking (MG, NM, BR, TW, IZ), pp. 600–616.
FME-2003-GurfinkelC #generative #model checking #multi: Generating Counterexamples for Multi-valued Model-Checking (AG, MC), pp. 503–521.
FME-2003-MorzentiPPS #model checking #specification: Model-Checking TRIO Specifications in SPIN (AM, MP, PSP, PS), pp. 542–561.
FME-2003-Schafer #analysis #fault #model checking #realtime: Combining Real-Time Model-Checking and Fault Tree Analysis (AS), pp. 522–541.
FME-2003-ThumsS #model checking: Model Checking FTA (AT, GS), pp. 739–757.
SEFM-2003-ShrotriBV #model checking #requirements #specification #visual notation: Model Checking Visual Specification of Requirements (US, PB, RV), pp. 202–209.
AGTIVE-2003-LaraGV #analysis #graph transformation #hybrid #metamodelling #model checking: Meta-Modelling, Graph Transformation and Model Checking for the Analysis of Hybrid Systems (JdL, EG, HV), pp. 292–298.
AdaEurope-2003-BliebergerB #evaluation #symbolic computation #using: Eliminating Redundant Range Checks in GNAT Using Symbolic Evaluation (JB, BB), pp. 153–167.
SEKE-2003-OwenM #lightweight #model checking #named: Lurch: a Lightweight Alternative to Model Checking (DO, TM), pp. 158–165.
UML-2003-Rouquette #architecture #uml: UML/MDA Reality Check: Heterogenous Architecture Style (NFR), p. 143.
UML-2003-SchmidtV #model checking #modelling #named #visual notation: CheckVML: A Tool for Model Checking Visual Modeling Languages (ÁS, DV), pp. 92–95.
OOPSLA-2003-ClarkeRN: Saving the world from bad beans: deployment-time confinement checking (DGC, MR, JN), pp. 374–387.
OOPSLA-2003-FahndrichL #object-oriented: Declaring and checking non-null types in an object-oriented language (MF, KRML), pp. 302–312.
SAC-2003-Paradkar #consistency #generative #interactive #modelling #self #testing #towards: Towards Model-Based Generation of Self-Priming and Self-Checking Conformance Tests for Interactive Systems (AMP), pp. 1110–1117.
ESEC-FSE-2003-GiannakopoulouM #model checking: Fluent model checking for event-based systems (DG, JM), pp. 257–266.
ESEC-FSE-2003-RobbyDH #framework #model checking #named: Bogor: an extensible and highly-modular software model checking framework (R, MBD, JH), pp. 267–276.
ESEC-FSE-2003-TkachukD #adaptation #analysis #composition #model checking: Adapting side effects analysis for modular program model checking (OT, MBD), pp. 188–197.
ICSE-2003-HongCLSU #data flow #model checking #testing: Data Flow Testing as Model Checking (HSH, SDC, IL, OS, HU), pp. 232–243.
CC-2003-BurrowsFW #runtime #source code #type checking: Run-Time Type Checking for Binary Programs (MB, SNF, JLW), pp. 90–105.
LCTES-2003-CorsaroC #java #performance #realtime: Efficient memory-reference checks for real-time java (AC, RC), pp. 51–58.
LCTES-2003-DhurjatiKAL #garbage collection #memory management #runtime #safety: Memory safety without runtime checks or garbage collection (DD, SK, VSA, CL), pp. 69–80.
CADE-2003-Clarke #abstraction #model checking #refinement #satisfiability: SAT-Based Counterexample Guided Abstraction Refinement in Model Checking (EMC), p. 1.
CADE-2003-DeplagneKKN #equation #induction #proving #theorem: Proof Search and Proof Check for Equational and Inductive Theorems (ED, CK, HK, QHN), pp. 297–316.
CAV-2003-AbdullaJNd #algorithm #model checking: Algorithmic Improvements in Regular Model Checking (PAA, BJ, MN, Jd), pp. 236–248.
CAV-2003-BartzisB #image #infinity #model checking #performance: Efficient Image Computation in Infinite State Model Checking (CB, TB), pp. 249–261.
CAV-2003-BordiniFPVW #model checking #multi #source code: Model Checking Multi-Agent Programs with CASP (RHB, MF, CP, WV, MW), pp. 110–113.
CAV-2003-CiardoS #model checking: Structural Symbolic CTL Model Checking of Asynchronous Systems (GC, RS), pp. 40–53.
CAV-2003-DongRS #model checking #proving: Evidence Explorer: A Tool for Exploring Model-Checking Proofs (YD, CRR, SAS), pp. 215–218.
CAV-2003-GlusmanK #consistency #model checking #specification: Model Checking Conformance with Scenario-Based Specifications (MG, SK), pp. 328–340.
CAV-2003-McMillan #model checking #satisfiability: Interpolation and SAT-Based Model Checking (KLM), pp. 1–13.
CAV-2003-MouraRS #bound #induction #model checking #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 #model checking #performance #μ-calculus: Fast μ-Calculus Model Checking when Tree-Width Is Bounded (JO), pp. 80–92.
CAV-2003-SeshiaB #automaton #bound #model checking #using: Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods (SAS, REB), pp. 154–166.
CSL-2003-KahlerW #complexity #ltl #model checking: Program Complexity of Dynamic LTL Model Checking (DK, TW), pp. 271–284.
CSL-2003-RybinaV #infinity #model checking #performance: Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture) (TR, AV), pp. 546–573.
FATES-2003-SenG #on the: On Checking Whether a Predicate Definitely Holds (AS, VKG), pp. 15–29.
ICLP-2003-Fages #model checking: Symbolic Model-Checking for Biochemical Systems (FF), p. 102.
LICS-2003-EmersonK #model checking #protocol: Model Checking Guarded Protocols (EAE, VK), pp. 361–370.
LICS-2003-Kwiatkowska #model checking #probability #theory and practice: Model checking for probability and time: from theory to practice (MZK), p. 351–?.
LICS-2003-Madhusudan #model checking: Model-checking Trace Event Structures (PM), pp. 371–380.
TestCom-2003-UralW #architecture #distributed #generative #sequence: Generating Checking Sequences for a Distributed Test Architecture (HU, CW), pp. 146–162.
TLCA-2003-Abel #termination: Termination and Productivity Checking with Continuous Types (AA0), pp. 1–15.
VMCAI-2003-DamsN #abstraction #analysis #model checking: Shape Analysis through Predicate Abstraction and Model Checking (DD, KSN), pp. 310–324.
VMCAI-2003-Masse #abstract interpretation #static analysis: Property Checking Driven Abstract Interpretation-Based Static Analysis (DM), pp. 56–69.
VMCAI-2003-PnueliZ #abstraction #model checking: Model-Checking and Abstraction to the Aid of Parameterized Systems (AP, LDZ), p. 4.
VMCAI-2003-Podelski #abstraction #model checking #refinement: Software Model Checking with Abstraction Refinement (AP), pp. 1–3.
VMCAI-2003-Sistla #model checking #reduction #symmetry: Symmetry Reductions in Model-Checking (APS), p. 25.
VMCAI-2003-YangRS #encoding #logic #mobile #model checking #process #using #π-calculus: A Logical Encoding of the pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution (PY, CRR, SAS), pp. 116–131.
ASE-2002-Crhova #composition #distributed #model checking: Distributed Modular Model Checking (JC), p. 312.
ASE-2002-HeimdahlCW #analysis #model checking: Deviation Analysis Through Model Checking (MPEH, YC, MWW), pp. 37–46.
ASE-2002-LoerH #analysis #interactive #model checking #towards: Towards Usable and Relevant Model Checking Techniques for the Analysis of Dependable Interactive Systems (KL, MDH), pp. 223–226.
DAC-2002-BartleyGB #comparison #pseudo #random testing #testing #verification: A comparison of three verification techniques: directed testing, pseudo-random testing and property checking (MB, DG, TB), pp. 819–823.
DAC-2002-CabodiCQ #bound #model checking #question #satisfiability: Can BDDs compete with SAT solvers on bounded model checking? (GC, PC, SQ), pp. 117–122.
DAC-2002-HartongHB #algorithm #model checking #verification: Model checking algorithms for analog verification (WH, LH, EB), pp. 542–547.
DAC-2002-JollyPM #automation #equivalence: Automated equivalence checking of switch level circuits (SJ, ANP, TM), pp. 299–304.
DAC-2002-ShengTH #effectiveness #safety #using: Effective safety property checking using simulation-based sequential ATPG (SS, KT, MSH), pp. 813–818.
DATE-2002-FavalliM #fault #problem #self: Problems Due to Open Faults in the Interconnections of Self-Checking Data-Paths (MF, CM), pp. 612–617.
DATE-2002-HartongHB #approach #model checking: An Approach to Model Checking for Nonlinear Analog Systems (WH, LH, EB), p. 1080.
DATE-2002-MetraSRF #online #power management #self #testing: Self-Checking Scheme for the On-Line Testing of Power Supply Noise (CM, LS, BR, MF), pp. 832–836.
ESOP-2002-Morrisett #type checking: Type Checking Systems Code (JGM), pp. 1–5.
FASE-2002-XieB #design #execution #model checking #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 #model checking #named #object-oriented: ObjectCheck: A Model Checking Tool for Executable Object-Oriented Software System Designs (FX, VL, JCB), pp. 331–335.
FoSSaCS-2002-JancarKMS #automaton #bound #proving: Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds (PJ, AK, FM, ZS), pp. 172–186.
FoSSaCS-2002-LangeS #fixpoint #logic #model checking: Model Checking Fixed Point Logic with Chop (ML, CS), pp. 250–263.
FoSSaCS-2002-LaroussinieMS #model checking #on the: On Model Checking Durational Kripke Structures (FL, NM, PS), pp. 264–279.
FoSSaCS-2002-Loding #infinity #model checking: Model-Checking Infinite Systems Generated by Ground Tree Rewriting (CL), pp. 280–294.
TACAS-2002-BallPR #abstraction #model checking #refinement: Relative Completeness of Abstraction Refinement for Software Model Checking (TB, AP, SKR), pp. 158–172.
TACAS-2002-BasuKPR #model checking #recursion #source code: Resource-Constrained Model Checking of Recursive Programs (SB, KNK, LRP, CRR), pp. 236–250.
TACAS-2002-EmersonK #model checking #resource management #scalability: Model Checking Large-Scale and Parameterized Resource Allocation Systems (EAE, VK), pp. 251–265.
TACAS-2002-GrocePY #adaptation #model checking: Adaptive Model Checking (AG, DP, MY), pp. 357–370.
TACAS-2002-KwiatkowskaNP #approach #hybrid #model checking #probability: Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach (MZK, GN, DP), pp. 52–66.
TACAS-2002-Mateescu #calculus #lts #model checking #μ-calculus: Local Model-Checking of Modal μ-Calculus on Acyclic Labeled Transition Systems (RM), pp. 281–295.
TACAS-2002-Ouaknine #abstraction #model checking: Digitisation and Full Abstraction for Dense-Time Model Checking (JO), pp. 37–51.
PEPM-2002-SecherS #graph: From checking to inference via driving and dag grammars (JPS, MHS), pp. 41–51.
PLDI-2002-FlanaganLLNSS #java #static analysis: Extended Static Checking for Java (CF, KRML, ML, GN, JBS, RS), pp. 234–245.
PLDI-2002-LeinoPZ #using: Using Data Groups to Specify and Check Side Effects (KRML, APH, YZ), pp. 246–257.
SAS-2002-GallardoMP #ltl #model checking #refinement: Refinement of LTL Formulas for Abstract Model Checking (MdMG, PM, EP), pp. 395–410.
SAS-2002-GiacobazziR #abstract interpretation #model checking: States vs. Traces in Model Checking by Abstract Interpretation (RG, FR), pp. 461–476.
SAS-2002-Hymans #abstract interpretation #behaviour #safety: Checking Safety Properties of Behavioral VHDL Descriptions by Abstract Interpretation (CH), pp. 444–460.
SAS-2002-LuK #type checking #type inference: Backward Type Inference Generalises Type Checking (LL, AK), pp. 85–101.
SAS-2002-RanzatoT #model checking: Making Abstract Model Checking Strongly Preserving (FR, FT), pp. 411–427.
STOC-2002-Ajtai #memory management: The invasiveness of off-line memory checking (MA), pp. 504–513.
CIAA-2002-Trahtman02a #testing: A Package TESTAS for Checking Some Kinds of Testability (ANT), pp. 228–232.
DLT-2002-Archangelsky #algorithm #equivalence #finite #multi #performance: Efficient Algorithm for Checking Multiplicity Equivalence for the Finite Z-Σ*-Automata (KA), pp. 283–289.
ICALP-2002-GenestMSZ #infinity #model checking: Infinite-State High-Level MSCs: Model-Checking and Realizability (BG, AM, HS, MZ), pp. 657–668.
FME-2002-CatanoH #java #specification #static analysis #using: Formal Specification and Static Checking of Gemplus’ Electronic Purse Using ESC/Java (NC, MH), pp. 272–289.
FME-2002-IoustinovaSS #model checking: Closing Open SDL-Systems for Model Checking with DTSpin (NI, NS, MS), pp. 531–548.
IFM-2002-WinterD #model checking #using: Model Checking Object-Z Using ASM (KW, RD), pp. 165–184.
AFP-2002-ClaessenRCHW02 #functional #lazy evaluation #quickcheck #source code #testing #using: Testing and Tracing Lazy Functional Programs Using QuickCheck and Hat (KC, CR, OC, JH, MW), pp. 59–99.
AdaEurope-2002-DewarHCW #ada #runtime: Exposing Uninitialized Variables: Strengthening and Extending Run-Time Checks in Ada (RD, OH, DC, PW), pp. 193–204.
CAiSE-2002-BenerecettiPST #model checking #multi #protocol #verification: Verification of Payment Protocols via MultiAgent Model Checking (MB, MP, LS, ST), pp. 311–327.
KR-2002-BaralZ #complexity #model checking: The Complexity of Model Checking for Knowledge Update (CB, YZ), pp. 82–96.
SEKE-2002-HeDD #architecture #model checking #specification: Model checking software architecture specifications in SAM (XH, JD, YD), pp. 271–278.
SEKE-2002-SantoneV #bytecode #java #model checking: Local model checking of Java bytecode (AS, GV), pp. 383–389.
SEKE-2002-SourrouilleC #constraints #modelling #uml: Constraint checking in UML modeling (JLS, GC), pp. 217–224.
POPL-2002-ChakiRR #message passing #model checking #modelling #source code: Types as models: model checking message-passing programs (SC, SKR, JR), pp. 45–57.
SAC-2002-BarbutiBF #abstract interpretation #bytecode #java #security: Checking security of Java bytecode by abstract interpretation (RB, CB, NDF), pp. 229–236.
SAC-2002-GallardoMMR #abstraction #model checking #using #xml: Using XML to implement abstraction for Model Checking (MdMG, JM, PM, ER), pp. 1021–1025.
FSE-2002-GurfinkelDC #logic #query: Model exploration with temporal logic query checking (AG, BD, MC), pp. 139–148.
FSE-2002-NimmerE #invariant #static analysis: Invariant inference for static checking (JWN, MDE), pp. 11–20.
ICSE-2002-ChandraGP #case study #industrial #model checking: Software model checking in practice: an industrial case study (SC, PG, CP), pp. 431–441.
CC-2002-QianHV #approach #array #bound #java: A Comprehensive Approach to Array Bounds Check Elimination for Java (FQ, LJH, CV), pp. 325–342.
OSDI-2002-KumarL #debugging #model checking #using: Using Model Checking to Debug Device Firmware (SK, KL), pp. 61–74.
OSDI-2002-MusuvathiPCED #approach #model checking #named: CMC: A Pragmatic Approach to Model Checking Real Code (MM, DYWP, AC, DRE, DLD), pp. 75–88.
CADE-2002-MouraRS #bound #infinity #lazy evaluation #model checking #proving #theorem proving: Lazy Theorem Proving for Bounded Model Checking over Infinite Domains (LMdM, HR, MS), pp. 438–455.
CADE-2002-StumpD #framework #logic #performance #proving: Faster Proof Checking in the Edinburgh Logical Framework (AS, DLD), pp. 392–407.
CAV-2002-AbdullaJMd #model checking: Regular Tree Model Checking (PAA, BJ, PM, Jd), pp. 555–568.
CAV-2002-AlurMY #behaviour #model checking #performance: Exploiting Behavioral Hierarchy for Efficient Model Checking (RA, MM, ZY), pp. 338–342.
CAV-2002-BarnerG #approximate #model checking #reduction #symmetry: Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking (SB, OG), pp. 93–106.
CAV-2002-BarrettDS #first-order #incremental #satisfiability: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (CWB, DLD, AS), pp. 236–249.
CAV-2002-BaumgartnerKA #analysis: Property Checking via Structural Analysis (JB, AK, JAA), pp. 151–165.
CAV-2002-BinghamH #bound #model checking: Semi-formal Bounded Model Checking (JDB, AJH), pp. 280–294.
CAV-2002-ChakrabartiAHJM #interface: Interface Compatibility Checking for Software Modules (AC, LdA, TAH, MJ, FYCM), pp. 428–441.
CAV-2002-ChatterjeeSG #consistency #memory management #model checking #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-CimattiCGGPRST #model checking: 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 #model checking #using: Automatic Abstraction Using Generalized Model Checking (PG, RJ), pp. 137–150.
CAV-2002-HartongHB #model checking #modelling #on the: On Discrete Modeling and Model Checking for Nonlinear Analog Systems (WH, LH, EB), pp. 401–413.
CAV-2002-Holzmann #analysis #model checking: Software Analysis and Model Checking (GJH), pp. 1–16.
CAV-2002-Jacobi #model checking #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: Model Checking Linear Properties of Prefix-Recognizable Systems (OK, NP, MYV), pp. 371–385.
CAV-2002-KurshanLY #model checking: Compressing Transitions for Model Checking (RPK, VL, HY), pp. 569–581.
CAV-2002-McMillan #bound #model checking #satisfiability: Applying SAT Methods in Unbounded Symbolic Model Checking (KLM), pp. 250–264.
CAV-2002-RajamaniR #consistency #message passing #modelling: Conformance Checking for Models of Asynchronous Message Passing Software (SKR, JR), pp. 166–179.
CAV-2002-RybinaV #canonical #infinity #model checking #using: Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking (TR, AV), pp. 386–400.
CAV-2002-TanC #model checking: Evidence-Based Model Checking (LT, RC), pp. 455–470.
CSL-2002-BeauquierRS #decidability #logic #model checking #probability: A Logic of Probability with Decidable Model-Checking (DB, AMR, AS), pp. 306–321.
ICLP-2002-CharatonikMP #constraints #infinity #model checking: Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP (WC, SM, AP), pp. 115–129.
ICLP-2002-PemmasaniRR #constraints #logic programming #model checking #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 #model checking #source code #using: Model checking Java programs using structural heuristics (AG, WV), pp. 12–21.
LICS-2002-ClarkeJLV #model checking: Tree-Like Counterexamples in Model Checking (EMC, SJ, YL, HV), pp. 19–29.
LICS-2002-LaplanteLMPR #abstraction #approach #model checking #probability #testing: Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing (SL, RL, FM, SP, MdR), pp. 30–39.
RTA-2002-DeharbeMR #logic #model checking: Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae (DD, AMM, CR), pp. 207–221.
RTA-2002-Durand #named #term rewriting: Autowrite: A Tool for Checking Properties of Term Rewriting Systems (ID), pp. 371–375.
SAT-2002-Clarke #abstraction #logic #model checking #refinement #satisfiability: SAT based abstraction refinement in temporal logic model checking (Keynote Talk) (EC), p. 26.
TestCom-2002-SerdarT #approach #finite #generative #sequence #state machine: A New Approach To Checking Sequence Generation for Finite State Machines (BS, KCT), p. 391–?.
VMCAI-2002-BernardeschiF #abstract interpretation #bytecode #java #model checking #security: Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode (CB, NDF), pp. 1–15.
VMCAI-2002-CimattiPRS #encoding #ltl #model checking #satisfiability: Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.
VMCAI-2002-Huth #model checking #using: Model Checking Modal Transition Systems Using Kripke Structures (MH), pp. 302–316.
VMCAI-2002-SidorovaS #model checking: Synchronous Closing of Timed SDL Systems for Model Checking (NS, MS), pp. 79–93.
VMCAI-2002-Tan #game studies: An Abstract Schema for Equivalence-Checking Games (LT), pp. 65–78.
ASE-2001-BarberGH #architecture #automation #development #feedback #model checking: 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 #model checking #static analysis: Combining Static Analysis and Model Checking for Software Analysis (GPB, WV), p. 262–?.
ASE-2001-Egyed #approach #consistency #scalability: Scalable Consistency Checking Between Diagrams-The ViewIntegra Approach (AE), pp. 387–390.
ASE-2001-InverardiMP #architecture #automation #consistency #modelling #using: Automated Check of Architectural Models Consistency Using SPIN (PI, HM, PP), pp. 346–349.
ASE-2001-Iosif #model checking #symmetry: Exploiting Heap Symmetries in Explicit-State Model Checking of Software (RI), pp. 254–261.
ASE-2001-NentwichEF #consistency #distributed #specification: Static Consistency Checking for Distributed Specifications (CN, WE, AF), p. 115–?.
ASE-2001-Romanovsky #concurrent #model checking #realtime: Model-Checking Real-Time Concurrent Systems (IR), p. 439.
ASE-2001-XieLB #execution #model checking #set #uml: Model Checking for an Executable Subset of UML (FX, VL, JCB), pp. 333–336.
DAC-2001-ChoiYLR #embedded #industrial #model checking: Model Checking of S3C2400X Industrial Embedded SOC Product (HC, BWY, YTL, HR), pp. 611–616.
DAC-2001-LiebmannLHG #design #logic: Enabling Alternating Phase Shifted Mask Designs for a Full Logic Gate Level: Design Rules and Design Rule Checking (LL, JL, FLH, IG), pp. 79–84.
DAC-2001-SchollB #equivalence #implementation: Checking Equivalence for Partial Implementations (CS, BB), pp. 238–243.
DATE-2001-GoldbergPB #equivalence #satisfiability #using: Using SAT for combinational equivalence checking (EIG, MRP, RKB), pp. 114–121.
DATE-2001-NovikovG #learning #multi #performance: An efficient learning procedure for multiple implication checks (YN, EIG), pp. 127–135.
DATE-2001-RedaS #diagrams #equivalence #satisfiability #using: Combinational equivalence checking using Boolean satisfiability and binary decision diagrams (SR, AS), pp. 122–126.
DATE-2001-RufHKR #multi: Simulation-guided property checking based on a multi-valued AR-automata (JR, DWH, TK, WR), pp. 742–748.
DocEng-2001-Tozawa #static typing #towards #type checking: Towards static type checking for XSLT (AT), pp. 18–27.
ICDAR-2001-KimKCS #recognition #segmentation: Legal Amount Recognition Based on the Segmentation Hypotheses for Bank Check Processing (KKK, JHK, YC, CYS), pp. 964–967.
ICDAR-2001-MoritaSEBS #recognition #word: Handwritten Month Word Recognition on Brazilian Bank Checks (MEM, RS, MAEY, FB, CYS), pp. 972–976.
ICDAR-2001-OliveiraSBS #composition: A Modular System to Recognize Numerical Amounts on Brazilian Bank Checks (LESdO, RS, FB, CYS), pp. 389–395.
ITiCSE-2001-Grissom #feedback: Reality check: an informal feedback tool (SG), p. 195.
FASE-J-1998-MotaS01 #industrial #model checking #tool support: Model-checking CSP-Z: strategy, tool support and industrial application (AM, AS), pp. 59–96.
ESOP-2001-Ranzato #model checking #on the: On the Completeness of Model Checking (FR), pp. 137–154.
ESOP-2001-XuRM #type system: Typestate Checking of Machine Code (ZX, TWR, BPM), pp. 335–351.
FASE-2001-LoginovYHR #debugging #runtime #type checking: Debugging via Run-Time Type Checking (AL, SHY, SH, TWR), pp. 217–232.
FASE-2001-NieseSMHBI #consistency #design #industrial #testing: Library-Based Design and Consistency Checking of System-Level Industrial Test Cases (ON, BS, TMS, AH, GB, HDI), pp. 233–248.
FASE-2001-PaigeO #consistency #metamodelling: Metamodelling and Conformance Checking with PVS (RFP, JSO), pp. 2–16.
FASE-2001-PingerE #communication #composition: Compositional Checking of Communication among Observers (RP, HDE), pp. 32–44.
FoSSaCS-2001-CharatonikDGMT #complexity #mobile #model checking: The Complexity of Model Checking Mobile Ambients (WC, SDZ, ADG, SM, JMT), pp. 152–167.
FoSSaCS-2001-LaroussinieMS #model checking: Model Checking CTL+ and FCTL is Hard (FL, NM, PS), pp. 318–331.
TACAS-2001-BallPR #abstraction #c #model checking #source code: Boolean and Cartesian Abstraction for Model Checking C Programs (TB, AP, SKR), pp. 268–283.
TACAS-2001-BolligLW #calculus #model checking #parallel #μ-calculus: Parallel Model Checking for the Alternation Free μ-Calculus (BB, ML, MW), pp. 543–558.
TACAS-2001-ChocklerKV #logic #metric #model checking: Coverage Metrics for Temporal Logic Model Checking (HC, OK, MYV), pp. 528–542.
TACAS-2001-CimattiRB #automaton #model checking #set: Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking (AC, MR, PB), pp. 313–327.
TACAS-2001-Finkbeiner #nondeterminism: Language Containment Checking with Nondeterministic BDDs (BF), pp. 24–38.
TACAS-2001-HuneRSV #automaton #linear #model checking #parametricity: Linear Parametric Model Checking of Timed Automata (TH, JR, MS, FWV), pp. 189–203.
TACAS-2001-Pandya #model checking: Model Checking CTL*[DC] (PKP), pp. 559–573.
TACAS-2001-PasareanuDV #java #model checking #source code: Finding Feasible Counter-examples when Model Checking Abstracted Java Programs (CSP, MBD, WV), pp. 284–298.
TACAS-2001-SebastianiTG #model checking #student: Model Checking Syllabi and Student Carreers (RS, AT, FG), pp. 128–142.
TACAS-2001-WilliamsAH #diagrams #satisfiability #using: Satisfiability Checking Using Boolean Expression Diagrams (PFW, HRA, HH), pp. 39–51.
SAS-2001-DorRS #analysis #c #integer #source code #string: Cleanness Checking of String Manipulations in C Programs via Integer Analysis (ND, MR, SS), pp. 194–212.
SAS-2001-GiacobazziQ #model checking: Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking (RG, EQ), pp. 356–373.
SAS-2001-Leino #static analysis: Applications of Extended Static Checking (KRML), pp. 185–193.
FLOPS-J1-1998-LedererD01 #automation #runtime #verification: Automatic Result Verification by Complete Run-Time Checking of Computations (EFAL, RAD), pp. 97–124.
ICALP-2001-BenediktGR #model checking #state machine #strict: Model Checking of Unrestricted Hierarchical State Machines (MB, PG, TWR), pp. 652–666.
ICALP-2001-GottlobP #clique #model checking: Hypergraphs in Model Checking: Acyclicity and Hypertree-Width versus Clique-Width (GG, RP), pp. 708–719.
FME-2001-ChechikEP #logic #model checking #multi: Model-Checking over Multi-valued Logics (MC, SME, VP), pp. 72–98.
FME-2001-LeuschelMC #csp #how #ltl #model checking #refinement: How to Make FDR Spin LTL Model Checking of CSP by Refinement (ML, TM, AC), pp. 99–118.
SEKE-2001-BarberGH #architecture #correctness #model checking #simulation #using: Evaluating Dynamic Correctness Properties of Domain Reference Architectures Using a Combination of Simulation and Model Checking (KSB, TJG, JH), pp. 19–28.
SEKE-2001-RamirezA #constraints #reasoning: Checking Integrity Constraints in Reasoning Systems based on Propositions and Relationships (JR, AdA), pp. 188–195.
LOPSTR-2001-LeuschelG #deduction #model checking #using: Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking (ML, SG), pp. 91–110.
PPDP-2001-Esparza #declarative #model checking #source code: Model Checking (with) Declarative Programs (JE), p. 37.
POPL-2001-NeculaR: Oracle-based checking of untrusted software (GCN, SPR), pp. 142–154.
RE-2001-FuxmanMPT #model checking #requirements #specification: Model Checking Early Requirements Specifications in Tropos (AF, JM, MP, PT), pp. 174–181.
ESEC-FSE-2001-ChoiRH #abstraction #automation #constraints #model checking: Automatic abstraction for model checking software systems with interrelated numeric constraints (YC, SR, MPEH), pp. 164–174.
ICSE-2001-AlurAGHKKMMW #design #model checking #named: JMOCHA: A Model Checking Tool that Exploits Design Structure (RA, LdA, RG, TAH, MK, CMK, RM, FYCM, BYW), pp. 835–836.
ICSE-2001-BerstelCRP #automation #design #formal method #scalability #user interface: A Scalable Formal Method for Design and Automatic Checking of User Interfaces (JB, SCR, GR, PSP), pp. 453–462.
ICSE-2001-BrylowDP #static analysis: Static Checking of Interrupt-Driven Software (DB, ND, JP), pp. 47–56.
ICSE-2001-Kaveh #design #model checking: Model Checking Distributd Objects Design (NK), pp. 793–794.
CAV-2001-Alfaro #model checking #web: Model Checking the World Wide Web (LdA), pp. 337–349.
CAV-2001-AlurW #implementation #network #protocol #refinement #verification: Verifying Network Protocol Implementations by Symbolic Refinement Checking (RA, BYW), pp. 169–181.
CAV-2001-AmlaEKN #diagrams #model checking #named #performance: Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams (NA, EAE, RPK, KSN), pp. 387–390.
CAV-2001-AsterothBA #model checking #modelling: Model Checking with Formula-Dependent Abstract Models (AA, CB, UA), pp. 155–168.
CAV-2001-BhatCG #automaton #model checking #performance: Efficient Model Checking Via Büchi Tableau Automata (GB, RC, AG), pp. 38–52.
CAV-2001-ChocklerKKV #approach #model checking: A Practical Approach to Coverage in Model Checking (HC, OK, RPK, MYV), pp. 66–78.
CAV-2001-CoptyFFGKTV #bound #industrial #model checking: Benefits of Bounded Model Checking at an Industrial Setting (FC, LF, RF, EG, GK, AT, MYV), pp. 436–453.
CAV-2001-GrumbergHS #calculus #distributed #model checking #μ-calculus: Distributed Symbolic Model Checking for μ-Calculus (OG, TH, AS), pp. 350–362.
CAV-2001-JhalaM #architecture #composition #model checking #verification: Microarchitecture Verification by Compositional Model Checking (RJ, KLM), pp. 396–410.
CAV-2001-JohannsenB #design #named: BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstarction (PJ), pp. 373–377.
CAV-2001-LevinY #model checking #named: SDLcheck: A Model Checking Tool (VL, HY), p. 377.
CAV-2001-Maidl #approach #model checking #safety: A Unifying Model Checking Approach for Safety Properties of Parameterized Systems (MM), pp. 311–323.
CAV-2001-ShanbhagGTAL #model checking #named: EASN: Integrating ASN.1 and Model Checking (VKS, KG, MT, AA, ML), pp. 382–386.
CAV-2001-SistlaG #model checking #symmetry: Symmetry and Reduced Symmetry in Model Checking (APS, PG), pp. 91–103.
CSL-2001-CharatonikT #decidability #mobile #model checking: The Decidability of Model Checking Mobile Ambients (WC, JMT), pp. 339–354.
IJCAR-2001-Pientka #higher-order #logic programming #reduction #source code #termination: Termination and Reduction Checking for Higher-Order Logic Programs (BP), pp. 401–415.
LICS-2001-BrunsG #logic #query: Temporal Logic Query Checking (GB, PG), pp. 409–417.
SAT-2001-SinzBK #implementation #named #parallel: PaSAT — Parallel SAT-Checking with Lemma Exchange: Implementation and Applications (CS, WB, WK), pp. 205–216.
ASE-2000-Bouhoula #confluence: Simultaneous Checking of Completeness and Ground Confluence (AB), p. 143–?.
ASE-2000-LiuR #automation #security #using: Automated Security Checking and Patching Using TestTalk (CL, DJR), pp. 261–264.
ASE-2000-ParkSSD #java #model checking: Java Model Checking (DYWP, US, JUS, DLD), pp. 253–256.
ASE-2000-VisserHBP #model checking #source code: Model Checking Programs (WV, KH, GPB, SP), pp. 3–12.
DAC-2000-BloemRS #model checking: Symbolic guided search for CTL model checking (RB, KR, FS), pp. 29–34.
DAC-2000-HuangC #composition #constraints: Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques (CYH, KTC), pp. 118–123.
DAC-2000-YangT #lazy evaluation #model checking: Lazy symbolic model checking (JY, AT), pp. 35–38.
DATE-2000-JangMH #model checking: Iterative Abstraction-Based CTL Model Checking (JYJ, IHM, GDH), pp. 502–507.
DATE-2000-SchonherrS #algorithm #automation #equivalence: Automatic Equivalence Check of Circuit Descriptions at Clocked Algorithmic and Register Transfer Level (JS, BS), p. 759.
DATE-2000-VardanianM #concurrent #detection #fault: Improving the Error Detection Ability of Concurrent Checkers by Observation Point Insertion in the Circuit Under Check (VAV, LBM), p. 762.
ESOP-2000-Charatonik #logic programming #source code #type checking: Directional Type Checking for Logic Programs: Beyond Discriminative Types (WC), pp. 72–87.
TACAS-2000-AlfaroKNPS #model checking #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 #model checking #protocol #security #using: Model Checking Security Protocols Using a Logic of Belief (MB, FG), pp. 519–534.
TACAS-2000-BharadwajS #automation #constraints #invariant #named #theorem proving: Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking (RB, SS), pp. 378–394.
TACAS-2000-BosnackiDHS #model checking: Model Checking SDL with Spin (DB, DD, LH, NS), pp. 363–377.
TACAS-2000-Bultan #concurrent #constraints #evaluation #model checking: BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems (TB), pp. 441–455.
TACAS-2000-CastilloW #model checking: Model Checking Support for the ASM High-Level Language (GDC, KW), pp. 331–346.
TACAS-2000-HelovuoV #process: Checking for CFFD-Preorder with Tester Processes (JH, AV), pp. 283–298.
TACAS-2000-HenzingerM #hybrid #model checking: Symbolic Model Checking for Rectangular Hybrid Systems (TAH, RM), pp. 142–156.
TACAS-2000-LarssonPY #model checking #on the #problem #traversal: On Memory-Block Traversal Problems in Model-Checking Timed-Systems (FL, PP, WY), pp. 127–141.
PLDI-2000-BodikGS #array #bound #named: ABCD: eliminating array bounds checks on demand (RB, RG, VS), pp. 321–333.
PLDI-2000-XuMR #safety: Safety checking of machine code (ZX, BPM, TWR), pp. 70–82.
SAS-2000-DorRS: Checking Cleanness in Linked Lists (ND, MR, SS), pp. 115–134.
SAS-2000-Podelski #constraints #model checking #theorem proving: Model Checking as Constraint Solving (AP), pp. 22–37.
SAS-2000-Saidi #abstraction #analysis #model checking: Model Checking Guided Abstraction and Analysis (HS), pp. 377–396.
ICALP-2000-EsparzaH #approach #ltl #model checking: A New Unfolding Approach to LTL Model Checking (JE, KH), pp. 475–486.
IFM-2000-HermannsKMS #algebra #model checking #probability #process #towards: Towards Model Checking Stochastic Process Algebra (HH, JPK, JMK, MS), pp. 420–439.
ICFP-2000-ClaessenH #haskell #lightweight #named #quickcheck #random testing #source code #testing: QuickCheck: a lightweight tool for random testing of Haskell programs (KC, JH), pp. 268–279.
EDOC-2000-KaramanolisGMW #model checking #workflow: Model Checking of Workflow Schemas (CTK, DG, JM, SMW), pp. 170–181.
ICPR-v4-2000-WatanabeOIK #analysis #video: Discourse Structure Analysis for News Video by Checking Surface Information in the Transcript (YW, YO, EI, SK), pp. 4242–4245.
KR-2000-Vidal #constraints #network: Controllability characterization and checking in Contingent Temporal Constraint Networks (TV), pp. 559–570.
UML-2000-AbdurazikO #collaboration #diagrams #generative #static analysis #testing #uml #using: Using UML Collaboration Diagrams for Static Checking and Test Generation (AA, AJO), pp. 383–395.
UML-2000-BottoniKPT #consistency #constraints #ocl #visualisation: Consistency Checking and Visualization of OCL Constraints (PB, MK, FPP, GT), pp. 294–308.
UML-2000-Kwon #model checking #semantics #uml: Rewrite rules and Operational Semantics for Model Checking UML Statecharts (GK), pp. 528–540.
TOOLS-EUROPE-2000-CornilsH #design pattern #documentation: Statically Checked Documentation with Design Patterns (AC, GH), pp. 419–430.
PPDP-2000-HanusS #functional #logic programming #nondeterminism #source code #type system: Type-based nondeterminism checking in functional logic programs (MH, FS), pp. 202–213.
ICSE-2000-Bultan #model checking #specification: Action Language: a specification language for model checking reactive systems (TB), pp. 335–344.
ICSE-2000-CorbettDHR #interface #java #model checking #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 #model checking #realtime: Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems (ZD, RAK), pp. 345–354.
ASPLOS-2000-ChouCEH #compilation #protocol #using: Using Meta-level Compilation to Check FLASH Protocol Code (AC, BC, DRE, MH), pp. 59–70.
ASPLOS-2000-KawahitoKN #effectiveness #hardware #null #pointer: Effective Null Pointer Check Elimination Utilizing Hardware Trap (MK, HK, TN), pp. 139–149.
OSDI-2000-EnglerCCH #compilation #using: Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions (DRE, BC, AC, SH), pp. 1–16.
CADE-2000-EmersonK #model checking: Reducing Model Checking of the Many to the Few (EAE, VK), pp. 236–254.
CADE-2000-Seger #float #model checking #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: Model Checking Continuous-Time Markov Chains by Transient Analysis (CB, BRH, HH, JPK), pp. 358–372.
CAV-2000-BehrmannHV #how #matter #model checking #order: Distributing Timed Model Checking — How the Search Order Matters (GB, TH, FWV), pp. 216–231.
CAV-2000-BouajjaniJNT #model checking: Regular Model Checking (AB, BJ, MN, TT), pp. 403–418.
CAV-2000-CassezL #constraints #hybrid #model checking: Model-Checking for Hybrid Systems by Quotienting and Constraints Solving (FC, FL), pp. 373–388.
CAV-2000-EsparzaHRS #algorithm #automaton #model checking #performance: Efficient Algorithms for Model Checking Pushdown Systems (JE, DH, PR, SS), pp. 232–247.
CAV-2000-McMillanQS #composition #induction #model checking: Induction in Compositional Model Checking (KLM, SQ, JBS), pp. 312–327.
CAV-2000-Shtrichman #bound #model checking #satisfiability: Tuning SAT Checkers for Bounded Model Checking (OS), pp. 480–494.
CAV-2000-WilliamsBCG #diagrams #model checking #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: Model Checking in HAL (MJGdlB, PJS, WH, KM), pp. 1270–1284.
CL-2000-JunttilaN #performance #satisfiability #towards: Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking (TAJ, IN), pp. 553–567.
CL-2000-MukhopadhyayP #logic #model checking #process: Model Checking for Timed Logic Processes (SM, AP), pp. 598–612.
CL-2000-NilssonL #constraints #logic programming #model checking: Constraint Logic Programming for Local and Symbolic Model-Checking (UN, JL), pp. 384–398.
CL-2000-PettorossiP #model checking: Perfect Model Checking via Unfold/Fold Transformations (AP, MP), pp. 613–628.
ISSTA-2000-Dill #java #model checking #source code: Model checking Java programs (abstract only) (DLD), p. 179.
WICSA-1999-Riemenschneider #architecture #correctness: Checking the Correctness of Architectural Transformation Steps via Proof-Carrying Architectures (RAR), pp. 65–82.
DAC-1999-BiereCCFZ #model checking #satisfiability #using: Symbolic Model Checking Using SAT Procedures instead of BDDs (AB, AC, EMC, MF, YZ), pp. 317–320.
DAC-1999-HoskoteKHZ #estimation #model checking: Coverage Estimation for Symbolic Model Checking (YVH, TK, PHH, XZ), pp. 300–305.
DATE-1999-FavalliM #design #functional #on the #self: On the Design of Self-Checking Functional Units Based on Shannon Circuits (MF, CM), pp. 368–375.
DATE-1999-Marques-SilvaG #equivalence #learning #recursion #satisfiability #using: Combinational Equivalence Checking Using Satisfiability and Recursive Learning (JPMS, TG), pp. 145–149.
DATE-1999-MeinelS #model checking #order #performance: Increasing Efficiency of Symbolic Model Checking by Accelerating Dynamic Variable Reordering (CM, CS), pp. 760–761.
DATE-1999-NoufalN #framework #generative #multi #self: A CAD Framework for Generating Self-Checking 1 Multipliers Based on Residue Codes (IAN, MN), p. 122–?.
DATE-1999-StrehlT #diagrams #model checking #petri net: Interval Diagram Techniques for Symbolic Model Checking of Petri Nets (KS, LT), pp. 756–757.
ICDAR-1999-GorskiAABPS #product line #recognition: A2iA Check Reader: A Family of Bank Check Recognition Systems (NG, VA, EA, OB, DP, JCS), pp. 523–526.
ICDAR-1999-KellandW #architecture #comparison #research: A Comparison of Research and Production Architectures for Check Reading Systems (SK, SW), pp. 99–102.
ICDAR-1999-KoerichL #automation #image #retrieval #visualisation: Automatic Storage, Retrieval, and Visualization of Bank Check Images (ALK, LLL), pp. 111–114.
ICDAR-1999-MadhvanathMM #image: Extracting Patron Data from Check Images (SM, SM, KMM), pp. 519–522.
ITiCSE-1999-PutSZ #network #student: The system of checking students’ knowledge with the use of wide area networks (DP, JS, MZ), p. 192.
FoSSaCS-1999-HuhnNW #communication #logic #model checking: Model Checking Logics for Communicating Sequential Agents (MH, PN, FW), pp. 227–242.
TACAS-1999-BiereCCZ #model checking: Symbolic Model Checking without BDDs (AB, AC, EMC, YZ), pp. 193–207.
TACAS-1999-DelzannoP #model checking: Model Checking in CLP (GD, AP), pp. 223–239.
PASTE-1999-ChandraR #c #physics #type checking: Physical Type Checking for C (SC, TWR), pp. 66–75.
WCRE-1999-DucasseRN #object-oriented #re-engineering: Type-Check Elimination: Two Object-Oriented Reengineering Patterns (SD, TR, RN), p. 157–?.
SAS-1999-Muller-OlmSS #model checking #named #tutorial: Model-Checking: A Tutorial Introduction (MMO, DAS, BS), pp. 330–354.
FLOPS-1999-BeierleM #approximate #prolog #source code #type checking #using: Using Types as Approximations for Type Checking Prolog Programs (CB, GM), pp. 251–266.
ICALP-1999-DickhoferW #automaton #model checking #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 #model checking #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 #model checking #testing #using: Feature Interaction Detection Using Testing and Model-Checking Experience Report (LdB), pp. 622–641.
FM-v1-1999-DeharbeM #fixpoint #model checking: Symbolic Model Checking with Fewer Fixpoint Computations (DD, AMM), pp. 272–288.
FM-v1-1999-KestenKPR #analysis #deduction #model checking #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 #model checking: Error Detection with Directed Symbolic Model Checking (FR, SE), pp. 195–211.
FM-v2-1999-ButhS #architecture #communication #design #model checking: Model-Checking the Architectural Design of a Fail-Safe Communication System for Railway Interlocking Systems (BB, MS), p. 1869.
IFM-1999-FischerW #model checking #specification: Model-Checking CSP-OZ Specifications with FDR (CF, HW), pp. 315–334.
IFM-1999-ReedSG #deduction #development #formal method #model checking #reasoning: Deductive Reasoning versus Model Checking: Two Formal Approaches for System Development (JNR, JES, FG), pp. 375–394.
CAiSE-1999-YiJ #process #reasoning #representation: Beyond Goal Representation: Checking Goal-Satisfaction by Temporal Reasoning with Business Processes (CHY, PJ), pp. 462–466.
UML-1999-Clark #diagrams #type checking #uml: Type Checking UML Static Diagrams (TC), pp. 503–517.
UML-1999-PaltorL #formal method #model checking #state machine #uml: Formalising UML State Machines for Model Checking (IP, JL), pp. 430–445.
LOPSTR-1999-Fribourg #constraints #logic programming #model checking: Constraint Logic Programming Applied to Model Checking (LF), pp. 30–41.
LOPSTR-1999-LeuschelM #abstract interpretation #infinity #model checking: Infinite State Model Checking by Abstract Interpretation and Program Specialisation (ML, TM), pp. 62–81.
ESEC-FSE-1999-Bokowski #constraints #java #named: CoffeeStrainer: Statically-Checked Constraints on the Definition and Use of Types in Java (BB), pp. 355–374.
ESEC-FSE-1999-FradetMP #architecture #consistency #multi: Consistency Checking for Multiple View Software Architectures (PF, DLM, MP), pp. 410–428.
ESEC-FSE-1999-GargantiniH #model checking #requirements #specification #testing #using: Using Model Checking to Generate Tests from Requirements Specifications (AG, CLH), pp. 146–162.
ESEC-FSE-1999-GiannakopoulouMK #question: Checking Progress with Action Priority: Is it Fair? (DG, JM, JK), pp. 511–527.
ESEC-FSE-1999-JaramilloGS #approach #comparison #debugging: Comparison Checking: An Approach to Avoid Debugging of Optimized Code (CJ, RG, MLS), pp. 268–284.
ICSE-1999-ChanABJNW #model checking #performance: Decoupling Synchronization from Local Control for Efficient Symbolic Model Checking of Statecharts (WC, RJA, PB, DHJ, DN, WEW), pp. 142–151.
ICSE-1999-NaumovichAC #analysis #concurrent #data flow #java #source code: Data Flow Analysis for Checking Properties of Concurrent Java Programs (GN, GSA, LAC), pp. 399–410.
CAV-1999-BasinFPV #bytecode #java #model checking #verification: Java Bytecode Verification by Model Checking (DAB, SF, JP, HV), pp. 491–494.
CAV-1999-BaumgartnerHSA #abstraction #algorithm #model checking: Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists (JB, TH, VS, AA), pp. 72–83.
CAV-1999-BiereCRZ #model checking #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 #model checking #performance: Efficient Decision Procedures for Model Checking of Linear Time Logic Properties (RB, KR, FS), pp. 222–235.
CAV-1999-BoppanaRTF #model checking: Model Checking Based on Sequential ATPG (VB, SPR, KT, MF), pp. 418–430.
CAV-1999-BrunsG #logic #model checking: Model Checking Partial State Spaces with 3-Valued Temporal Logics (GB, PG), pp. 274–287.
CAV-1999-JeronM #generative #model checking #testing: Test Generation Derived from Model-Checking (TJ, PM), pp. 108–121.
CAV-1999-KupfermanV #model checking #safety: Model Checking of Safety Properties (OK, MYV), pp. 172–183.
CAV-1999-Lind-NielsenA #model checking: Stepwise CTL Model Checking of State/Event Systems (JLN, HRA), pp. 316–327.
CAV-1999-ManoliosNS #bisimulation #model checking #proving #theorem proving: Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation (PM, KSN, RS), pp. 369–379.
CAV-1999-SaidiS: Abstract and Model Check While You Prove (HS, NS), pp. 443–454.
CAV-1999-YangSBO #constraints #model checking #modelling #optimisation: Optimizing Symbolic Model Checking for Constraint-Rich Models (BY, RGS, REB, DRO), pp. 328–340.
CSL-1999-GeuversPZ #proving #type system: Safe Proof Checking in Type Theory with Y (HG, EP, JZ), pp. 439–452.
DAC-1998-PardoH #incremental #model checking #using: Incremental CTL Model Checking Using BDD Subsetting (AP, GDH), pp. 457–462.
DATE-1998-Eijk #equivalence #traversal: Sequential Equivalence Checking without State Space Traversal (CAJvE), pp. 618–623.
DATE-1998-GongCK #architecture #synthesis: Architectural Rule Checking for High-level Synthesis (JG, CTC, KK), pp. 949–950.
FASE-1998-MotaS #model checking: Model-Checking CSP-Z (AM, AS), pp. 205–220.
TACAS-1998-AcetoBL #automaton #model checking #reachability #testing: Model Checking via Reachability Testing for Timed Automata (LA, AB, KGL), pp. 263–280.
TACAS-1998-AjamiHI #linear #logic #model checking #symmetry: Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond (KA, SH, JMI), pp. 52–67.
TACAS-1998-DawsT #abstraction #model checking #reachability #realtime #using: Model Checking of Real-Time Reachability Properties Using Abstractions (CD, ST), pp. 313–329.
TACAS-1998-LasterG #composition #model checking: Modular Model Checking of Software (KL, OG), pp. 20–35.
TACAS-1998-StevensS #game studies #model checking #using: Practical Model-Checking Using Games (PS, CS), pp. 85–101.
PLDI-1998-XiP #array #bound #dependent type: Eliminating Array Bound Checking Through Dependent Types (HX, FP), pp. 249–257.
SAS-1998-Levi #model checking #semantics: A Symbolic Semantics for Abstract Model Checking (FL), pp. 134–151.
SAS-1998-SchmidtS #abstract interpretation #model checking #program analysis: Program Analysis as Model Checking of Abstract Interpretations (DAS, BS), pp. 351–380.
STOC-1998-LewinV #polynomial #question #towards: Checking Polynomial Identities over any Field: Towards a Derandomization? (DL, SPV), pp. 438–447.
ICALP-1998-Henzinger #game studies #model checking #multi: Model Checking Game Properties of Multi-agent Systems (Abstract) (TAH), p. 543.
ICALP-1998-LiC #bisimulation #congruence #π-calculus: Checking Strong/Weak Bisimulation Equivalences and Observation Congruence for the π-Calculus (ZL, HC), pp. 707–718.
ICPR-1998-KaufmannB #fault #locality #using: Amount translation and error localization in check processing using syntax-directed translation (GK, HB), pp. 1530–1534.
KR-1998-CervesatoFM #calculus #complexity #model checking #quantifier: The Complexity of Model Checking in Modal Event Calculi with Quantifiers (IC, MF, AM), pp. 368–379.
TOOLS-ASIA-1998-NiZ #automation #constraints #dynamic analysis #java #semantics: An Automatically Dynamic Checking Tool for Java Beans Semantic Constraints (BN, ZZ), pp. 164–172.
ALP-PLILP-1998-CuiDDKRRRSW #logic programming #model checking: 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 #model checking: Data Flow Analysis is Model Checking of Abstract Interpretations (DAS), pp. 38–48.
ICRE-1998-SchneiderECH #fault tolerance #model checking #requirements #using #validation: Validating Requirements for Fault Tolerant Systems using Model Checking (FS, SME, JRC, GJH), pp. 4–13.
FSE-1998-AlurY #model checking #state machine: Model Checking of Hierarchical State Machines (RA, MY), pp. 175–188.
FSE-1998-DwyerP #model checking: Filter-Based Model Checking of Partial Systems (MBD, CSP), pp. 189–202.
CAV-1998-AlurHMQRT #composition #model checking #named: MOCHA: Modularity in Model Checking (RA, TAH, FYCM, SQ, SKR, ST), pp. 521–525.
CAV-1998-BeerBL #model checking #on the fly: On-the-Fly Model Checking of RCTL Formulas (IB, SBD, AL), pp. 184–194.
CAV-1998-Bolignano #encryption #model checking #protocol #verification: Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols (DB), pp. 77–87.
CAV-1998-BozgaDMOTY #model checking #named #realtime: Kronos: A Model-Checking Tool for Real-Time Systems (MB, CD, OM, AO, ST, SY), pp. 546–550.
CAV-1998-ClarkeEJS #model checking #reduction #symmetry: Symmetry Reductions inModel Checking (EMC, EAE, SJ, APS), pp. 147–158.
CAV-1998-Daws #model checking #named #realtime: Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems (CD), pp. 542–545.
CAV-1998-HenzingerKQ #model checking: From Pre-historic to Post-modern Symbolic Model Checking (TAH, OK, SQ), pp. 195–206.
CAV-1998-Holzmann #model checking #on the: On Checking Model Checkers (GJH), pp. 61–70.
CAV-1998-KaufmannMP #constraints #design #model checking: Design Constraints in Symbolic Model Checking (MK, AM, CP), pp. 477–487.
CAV-1998-MankuHB #model checking #symmetry: Structural Symmetry and Model Checking (GSM, RH, RKB), pp. 159–171.
CAV-1998-McMillan #algorithm #composition #implementation #model checking #verification: Verification of an Implementation of Tomasulo’s Algorithm by Compositional Model Checking (KLM), pp. 110–121.
CAV-1998-NalumasuGMG #approach #memory management #model checking #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 #model checking #using: Model Checking LTL Using Net Unforldings (FW), pp. 207–218.
CAV-1998-Wilding #policy #proving #realtime #scheduling: A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy (MW), pp. 369–378.
CAV-1998-XuCSCM #first-order #graph #logic #model checking #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 #model checking #performance #requirements: Improving Efficiency of Symbolic Model Checking for State-Based System Requirements (WC, RJA, PB, DN), pp. 102–112.
ISSTA-1998-GodefroidHJ #analysis #model checking #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 #model checking #nondeterminism #on the: On Model Checking for Non-Deterministic Infinite-State Systems (EAE, KSN), pp. 70–80.
DAC-1997-KuehlmannK #equivalence #using: Equivalence Checking Using Cuts and Heaps (AK, FK), pp. 263–268.
EDTC-1997-AbdullaRK #embedded #multi: A scheme for multiple on-chip signature checking for embedded SRAMs (MFA, CPR, AK), p. 625.
EDTC-1997-KropfR #model checking #using: Using MTBDDs for discrete timed symbolic model checking (TK, JR), pp. 182–187.
EDTC-1997-PaschalisGGK #fault #self: A totally self-checking 1-out-of-3 code error indicator (AMP, NG, DG, PK), pp. 450–454.
ICDAR-1997-DjeziriNP: Extraction of Items From Checks (SD, FN, RP), pp. 749–752.
ICDAR-1997-WongMX #fault tolerance #recognition: A Chinese Bank Check Recognition System Based on the Fault Tolerant Technique (SW, FM, SX), pp. 1038–1042.
VLDB-1997-LlirbatST #transaction #using: Using Versions in Update Transactions: Application to Integrity Checking (FL, ES, DT), pp. 96–105.
TACAS-1997-AndersenSM #model checking: Partial Model Checking with ROBDDs (HRA, JS, NM), pp. 35–49.
TACAS-1997-EngelsFM #generative #model checking #network #testing #using: Test Generation for Intelligent Networks Using Model Checking (AE, LMGF, SM), pp. 384–398.
TACAS-1997-OwreRS #integration #model checking: Integration in PVS: Tables, Types, and Model Checking (SO, JMR, NS), pp. 366–383.
TACAS-1997-Penczek #model checking #subclass: Model-Checking for a Subclass of Event Structures (WP), pp. 145–164.
ICALP-1997-BaierCHKR #model checking #probability #process: Symbolic Model Checking for Probabilistic Processes (CB, EMC, VHG, MZK, MR), pp. 430–440.
ICALP-1997-BurkartS #calculus #infinity #model checking #process #μ-calculus: Model Checking the Full Modal μ-Calculus for Infinite Sequential Processes (OB, BS), pp. 419–429.
ICALP-1997-CodenottiEGK: Checking Properties of Polynomials (Extended Abstract) (BC, FE, PG, RK), pp. 203–213.
FME-1997-Gregoire #protocol #proving #using: TLA + PROMELA: Conjecture, Check, Proof, Engineering New Protocols Using Methods and Formal Notations (JCG), pp. 378–397.
POPL-1997-BourdoncleM #higher-order #multi #polymorphism: Type-Checking Higher-Order Polymorphic Multi-Methods (FB, SM), pp. 302–315.
POPL-1997-Godefroid #model checking #programming language #using: Model Checking for Programming Languages using Verisoft (PG), pp. 174–186.
SAC-1997-SiLL #detection #documentation #named: CHECK: a document plagiarism detection system (AS, HVL, RWHL), pp. 70–77.
ESEC-FSE-1997-DwyerCH #abstraction #model checking #user interface #using #visual notation: Model Checking Graphical User Interfaces Using Abstractions (MBD, VC, LH), pp. 244–261.
ICSE-1997-AlurJKO #case study #experience #model checking #realtime: Model-Checking of Real-Time Systems: A Telecommunications Application (Experience Report) (RA, LJJ, JJK, JVO), pp. 514–524.
ICSE-1997-FernandezR #automation #specification: Automatic Checking of Instruction Specifications (MFF, NR), pp. 326–336.
CADE-1997-Vardi #automaton #logic: Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics (MYV), pp. 191–206.
CAV-1997-BarrettM #design #model checking: Model Checking in a Microprocessor Design Project (GB, AM), pp. 214–225.
CAV-1997-BeerBEGGHLPRRW #model checking #named: RuleBase: Model Checking at IBM (IB, SBD, CE, DG, LG, TH, AL, PP, YR, GR, YW), pp. 480–483.
CAV-1997-Biere #calculus #model checking #named #performance #μ-calculus: μcke — Efficient μ-Calculus Model Checking (AB), pp. 468–471.
CAV-1997-BultanGP #infinity #model checking #using: Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic (TB, RG, WP), pp. 400–411.
CAV-1997-ChanABN #constraints #model checking #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 #model checking #on the fly #symmetry: On-the-Fly Model Checking Under Fairness That Exploits Symmetry (VG, APS), pp. 232–243.
CAV-1997-ImmermanV #logic #model checking #transitive: Model Checking and Transitive-Closure Logic (NI, MYV), pp. 291–302.
CAV-1997-KestenMMPS #model checking: Symbolic Model Checking with Rich ssertional Languages (YK, OM, MM, AP, ES), pp. 424–435.
CAV-1997-KupfermanV #revisited: Module Checking Revisited (OK, MYV), pp. 36–47.
CAV-1997-LindenstraussSS #logic programming #named #query #source code #termination: TermiLog: A System for Checking Termination of Queries to Logic Programs (NL, YS, AS), pp. 444–447.
CAV-1997-MelzerR #concurrent #using: Deadlock Checking Using Net Unfoldings (SM, SR), pp. 352–363.
CAV-1997-PardoH #abstraction #automation #calculus #model checking #μ-calculus: Automatic Abstraction Techniques for Propositional μ-calculus Model Checking (AP, GDH), pp. 12–23.
CAV-1997-RamakrishnanRRSSW #model checking #performance #using: Efficient Model Checking Using Tabled Resolution (YSR, CRR, IVR, SAS, TS, DSW), pp. 143–154.
ICLP-1997-CervesatoFM #calculus #complexity #model checking: The Complexity of Model Checking in Modal Event Calculi (IC, MF, AM), p. 419.
ILPS-1997-Clarke #logic #model checking: Temporal Logic Model Checking (Abstract) (EMC), p. 3.
ILPS-1997-Gerth #model checking: Model Checking (Abstract) (RG), p. 39.
LICS-1997-HuthK #analysis #model checking: Quantitative Analysis and Model Checking (MH, MZK), pp. 111–122.
DAC-1996-ClarkeKZ #fault #model checking #word: Word Level Model Checking — Avoiding the Pentium FDIV Error (EMC, MK, XZ), pp. 645–648.
DAC-1996-KantrowitzN #analysis #correctness #simulation #verification #what: I’m Done Simulating: Now What? Verification Coverage Analysis and Correctness Checking of the DECchip 21164 Alpha Microprocessor (MK, LMN), pp. 325–330.
SIGMOD-1996-RossSS #constraints #maintenance: Materialized View Maintenance and Integrity Constraint Checking: Trading Space for Time (KAR, DS, SS), pp. 447–458.
VLDB-1996-LeeL #constraints #database #deduction: Further Improvements on Integrity Constraint Checking for Stratifiable Deductive Databases (SYL, TWL), pp. 495–505.
ESOP-1996-FradetCM #algorithm #axiom #detection #fault #pointer #static analysis: Static Detection of Pointer Errors: An Axiomatisation and a Checking Algorithm (PF, RC, DLM), pp. 125–140.
ESOP-1996-MelzerE #integer #programming: Checking System Properties via Integer Programming (SM, JE), pp. 250–264.
ESOP-1996-RohwedderP #higher-order #logic programming #source code #termination: Mode and Termination Checking for Higher-Order Logic Programs (ER, FP), pp. 296–310.
TACAS-1996-BhatC #calculus #model checking #μ-calculus: Efficent Local Model-Checking for Fragments of teh Modal μ-Calculus (GB, RC), pp. 107–126.
TACAS-1996-ChouP #model checking #partial order #reduction #verification: Formal Verification of a Partial-Order Reduction Technique for Model Checking (CTC, DP), pp. 241–257.
SAS-1996-CrnogoracKS #comparison: A Comparison of Three Occur-Check Analysers (LC, ADK, HS), pp. 159–173.
STOC-1996-FrankelGY #encryption #robust: Witness-Based Cryptographic Program Checking and Robust Function Sharing (YF, PG, MY), pp. 499–508.
FME-1996-BoigelotG #analysis #model checking #protocol #using: Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN (BB, PG), pp. 465–478.
FME-1996-HavelundS #model checking #protocol #proving #theorem proving #verification: Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.
ICFP-1996-Ghelli #complexity #kernel #type checking #type system: Complexity of Kernel Fun Subtype Checking (GG), pp. 134–145.
POPL-1996-JacksonJD #performance #specification: Faster Checking of Software Specifications by Eliminating Isomorphs (DJ, SJ, CD), pp. 79–90.
FSE-1996-AndersonBBCMNR #model checking #scalability #specification: Model Checking Large Software Specifications (RJA, PB, SB, WC, FM, DN, JDR), pp. 156–166.
FSE-1996-DamonJJ #diagrams #relational #specification: Checking Relational Specifications With Binary Decision Diagrams (CD, DJ, SJ), pp. 70–80.
ICSE-1996-CheungK #analysis #composition #reachability #safety: Checking Subsystem Safety Properties in Compositional Reachability Analysis (SCC, JK), pp. 144–154.
CAV-1996-Avrunin #algebra #geometry #model checking #using: Symbolic Model Checking Using Algebraic Geometry (GSA), pp. 26–37.
CAV-1996-CamposG #analysis #model checking #verification: Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System (SVAC, OG), pp. 257–268.
CAV-1996-ClarkeMCH #model checking: Symbolic Model Checking (EMC, KLM, SVAC, VHG), pp. 419–427.
CAV-1996-KupfermanV: Module Checking (OK, MYV), pp. 75–86.
CAV-1996-McMillan #model checking #representation: A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking (KLM), pp. 13–25.
CAV-1996-OwreRRSS #model checking #named #proving #specification: PVS: Combining Specification, Proof Checking, and Model Checking (SO, SR, JMR, NS, MKS), pp. 411–414.
CAV-1996-ShuklaHR #game studies #model checking #verification: HORNSAT, Model Checking, Verification and games (Extended Abstract) (SKS, HBHI, DJR), pp. 99–110.
CAV-1996-SipmaUM #deduction #model checking: Deductive Model Checking (HS, TEU, ZM), pp. 208–219.
CAV-1996-Walukiewicz #automaton #game studies #model checking #process: Pushdown Processes: Games and Model Checking (IW), pp. 62–74.
ISSTA-1996-BultanFG #composition #model checking #verification: Compositional Verification by Model Checking for Counter-Examples (TB, JF, RG), pp. 224–238.
LICS-1996-AlurMP #concurrent #correctness #model checking: Model-Checking of Correctness Conditions for Concurrent Objects (RA, KLM, DP), pp. 219–228.
LICS-1996-BhatC #calculus #equation #model checking #performance #μ-calculus: Efficient Model Checking via the Equational μ-Calculus (GB, RC), pp. 304–312.
LICS-1996-WillemsW #branch #linear #model checking #partial order: Partial-Order Methods for Model Checking: From Linear Time to Branching Time (BW, PW), pp. 294–303.
DAC-1995-BormannLPV #design #hardware #industrial #model checking: Model Checking in Industrial Hardware Design (JB, JL, MP, GV), pp. 298–303.
DAC-1995-ClarkeGMZ #generative #model checking #performance: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking (EMC, OG, KLM, XZ), pp. 427–432.
DAC-1995-ZhouB #canonical #equivalence: Equivalence Checking of Datapaths Based on Canonical Arithmetic Expressions (ZZ, WB), pp. 546–551.
ICDAR-v1-1995-LethelierLG #automation: An automatic reading system for handwritten numeral amounts on French checks (EL, ML, MG), pp. 92–97.
ICDAR-v2-1995-AgarwalGHGW #detection: Detection of courtesy amount block on bank checks (AA, LG, KH, AG, PSPW), pp. 748–751.
ICDAR-v2-1995-ChinW #recognition: A microprocessor-based optical character recognition check reader (FYLC, FW), pp. 982–985.
TACAS-1995-FrancescoFGI #approximate #finite #model checking #process: Model Checking of Non-Finite State Processes by Finite Approximations (NDF, AF, SG, PI), pp. 195–215.
TACAS-1995-Mader #calculus #model checking #μ-calculus: Modal μ-Calculus, Model Checking and Gauß Elimination (AM), pp. 72–88.
TACAS-1995-MullerN #deduction #model checking: Combining Model Checking and Deduction for I/O-Automata (OM, TN), pp. 1–16.
TACAS-1995-RoscoeGGHJS #concurrent #csp #how #model checking: Hierarchical Compression for Model-Checking CSP or How to Check 1020 Dining Philosophers for Deadlock (AWR, PHBG, MG, JRH, DMJ, JBS), pp. 133–152.
PEPM-1995-Cridlig #analysis #concurrent #model checking #semantics #using: Semantic Analysis of Shared-Memory Concurrent Languages using Abstract Model-Checking (RC), pp. 214–225.
PEPM-1995-LeuschelS #partial evaluation #towards: Towards Creating Specialised Integrity Checks through Partial Evaluation of Meta-Interpreters (ML, DDS), pp. 253–263.
PLDI-1995-KolteW #array: Elimination of Redundant Array Subscript Range Checks (PK, MW), pp. 270–278.
SAS-1995-CleavelandIY #abstraction #model checking: Optimality in Abstractions of Model Checking (RC, SPI, DY), pp. 51–63.
SAS-1995-JagannathanW #analysis #effectiveness #runtime: Effective Flow Analysis for Avoiding Run-Time Checks (SJ, AKW), pp. 207–224.
AdaEurope-1995-RognesS #ada #performance: Performance Tuning of a Check-Out System Coded in Ada (BR, PIS), pp. 99–110.
CIKM-1995-HerzogS #constraints #execution #parallel: Parallel Execution of Integrity Constraint Checks (UH, RS), pp. 82–89.
SEKE-1995-LinL #message passing #model checking #protocol #verification: Formal Verification of a Message-Passing Protocol with Model Checking (AL, FL), pp. 296–302.
RE-1995-HeitmeyerLK #consistency #requirements #specification: Consistency checking of SCR-style requirements specifications (CLH, BGL, DLK), pp. 56–65.
FSE-1995-WingV #case study #model checking: Model Checking Software Systems: A Case Study (JMW, MV), pp. 128–139.
CAV-1995-AndersenV #behaviour #fixpoint #performance #using: Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion (HRA, BV), pp. 142–154.
CAV-1995-DingelF #abstraction #infinity #model checking #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 #model checking #tutorial #μ-calculus: Methods for μ-calculus Model Checking: A Tutorial (Abstract) (EAE), p. 141.
CAV-1995-EmersonS #approach #model checking #symmetry: Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach (EAE, APS), pp. 309–324.
CAV-1995-EsparzaK #branch #logic #model checking #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 #model checking #proving: An Integration of Model Checking with Automated Proof Checking (SR, NS, MKS), pp. 84–97.
CAV-1995-SokolskyS #model checking #realtime: Local Model Checking for Real-Time Systems (Extended Abstract) (OS, SAS), pp. 211–224.
ICLP-1995-FormicaMT #database #object-oriented #proving #satisfiability #theorem proving: A Theorem Prover for Checking Satisfiability of Object-Oriented Database Schemas (AF, MM, RT), p. 819.
ILPS-1995-LeuschelM #deduction #representation: Partial Deduction of the Ground Representation and its Application to Integrity Checking (ML, BM), pp. 495–509.
LICS-1995-AlurPP #model checking: Model-Checking of Causality Properties (RA, DP, WP), pp. 90–100.
LICS-1995-Andersen #model checking: Partial Model Checking (Extended Abstract) (HRA), pp. 398–407.
LICS-1995-BhatCG #model checking #on the fly #performance: Efficient On-the-Fly Model Checking for CTL* (GB, RC, OG), pp. 388–397.
LICS-1995-Vardi #complexity #composition #model checking #on the: On the Complexity of Modular Model Checking (MYV), pp. 101–111.
EDAC-1994-ChenYF #debugging #design #identification #model checking: Bug Identification of a Real Chip Design by Symbolic Model Checking (BC, MY, MF), pp. 132–136.
EDAC-1994-HirechFGR #design #simulation #testing: A Redefinable Symbolic Simulation Technique to Testability Design Rules Checking (MH, OF, AG, EHR), p. 668.
EDAC-1994-NicolaidisB #array #implementation #multi #performance #self: Efficient Implementations of Self-Checking Multiply and Divide Arrays (MN, HB), pp. 574–579.
PODS-1994-GuptaSUW #constraints: Constraint Checking with Partial Information (AG, YS, JDU, JW), pp. 45–55.
ESOP-1994-CorsiniR #constraints #logic programming #model checking: Symbolic Model Checking and Constraint Logic Programming: a Cross-Fertilization (MMC, AR), pp. 180–194.
SAS-1994-AikenL #logic programming #source code #type checking: Directional Type Checking of Logic Programs (AA, TKL), pp. 43–60.
ICALP-1994-VergauwenL #correctness #equation #performance: Efficient Local Correctness Checking for Single and Alternating Boolean Equation Systems (BV, JL), pp. 304–315.
FME-1994-Jackson #infinity #model checking #specification: Abstract Model Checking of Infinite Specifications (DJ), pp. 519–531.
AdaEurope-1994-Moller #ada #runtime: Run-Time Check Elimination for Ada 9X (PLM), pp. 11–23.
TRI-Ada-1994-Moller #ada #runtime: Run-Time Check Elimination for Ada 9X (PLM), pp. 122–128.
FSE-1994-DillonY #concurrent: Oracles for Checking Temporal Properties of Concurrent Systems (LKD, QY), pp. 140–153.
FSE-1994-EvansGHT #named #specification #using: LCLint: A Tool for Using Specifications to Check Code (DE, JVG, JJH, YMT), pp. 87–96.
CAV-1994-AzizSS #composition #equivalence #model checking: Formula-Dependent Equivalence for Compositional CTL Model Checking (AA, TRS, VS), pp. 324–337.
CAV-1994-BernholtzVW #approach #model checking: An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract) (OB, MYV, PW), pp. 142–155.
CAV-1994-ClarkeGH #ltl #model checking: Another Look at LTL Model Checking (EMC, OG, KH), pp. 415–427.
CAV-1994-DamsGDHKP #abstraction #adaptation #model checking #using: Model Checking Using Adaptive State and Data Abstraction (DD, RG, GD, RH, PK, HP), pp. 455–467.
CAV-1994-GeistB #automation #model checking #performance: Efficient Model Checking by Automated Ordering of Transition Relation Partitions (DG, IB), pp. 299–310.
CAV-1994-Hungar #metaprogramming #model checking #process: Model Checking of macro Processes (HH), pp. 169–181.
CAV-1994-Kurshan #modelling: Models Whose Checks Don’t Explode (RPK), pp. 222–233.
CAV-1994-Manna #model checking: Beyond Model Checking (ZM), pp. 220–221.
CAV-1994-McMillan #model checking: Hierarchical Representations of Discrete Functions, with Application to Model Checking (KLM), pp. 41–54.
CAV-1994-NaikS #model checking #modelling #protocol #using #verification: Modeling and Verification of a Real Life Protocol Using Symbolic Model Checking (VGN, APS), pp. 194–206.
CAV-1994-Peled #model checking #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 #model checking #μ-calculus: Incremental Model Checking in the Modal μ-Calculus (OS, SAS), pp. 351–363.
ICLP-1994-DeckerC #database #deduction: A Slick Procedure for Integrity Checking in Deductive Databases (HD, MC), pp. 456–469.
ILPS-1994-Brisset #logic programming #polymorphism #programming language #type checking: Avoiding Dynamic Type Checking in a Polymorphic Logic Programming Language (PB), p. 674.
LICS-1994-Wells #decidability #higher-order #λ-calculus: Typability and Type-Checking in the Second-Order λ-Calculus are Equivalent and Undecidable (JBW), pp. 176–185.
LICS-1994-ZhangSS #calculus #complexity #model checking #on the #parallel #μ-calculus: On the Parallel Complexity of Model Checking in the Modal μ-Calculus (SZ, OS, SAS), pp. 154–163.
DAC-1993-HojatiSBK #approach #model checking: A Unified Approach to Language Containment and Fair CTL Model Checking (RH, TRS, RKB, RPK), pp. 475–481.
PODS-1993-ChomickiN #constraints #on the: On the Feasibility of Checking Temporal Integrity Constraints (JC, DN), pp. 202–213.
STOC-1993-ArBCG #approximate: Checking approximate computations over the reals (SA, MB, BC, PG), pp. 786–795.
DLT-1993-JurvanenPT: Tree Languages Recognizable by Regular Frontier Check (EJ, AP, WT), pp. 3–17.
ICALP-1993-Blum #approach #reliability #source code: Program Result Checking: A New Approach to Making Programs More Reliable (MB), pp. 1–14.
ICALP-1993-HungarS #model checking #process: Local Model Checking for Context-Free Processes (HH, BS), pp. 593–605.
FME-1993-Barrett #model checking: Model Checking in Practice — The T9000 Virtual Channel Processor (GB), pp. 129–147.
FME-1993-CraigenGR #formal method #industrial: Formal Methods Reality Check: Industrial Usage (DC, SLG, TR), pp. 250–267.
FME-1993-WangME #distributed #model checking #realtime: Symbolic Model Checking for Distributed Real-Time Systems (FW, AKM, EAE), pp. 632–651.
HCI-ACS-1993-TakedaHS: The Fatigue Check System for VDT Workers by Measuring CFF (MT, YH, KS), pp. 618–623.
SEKE-1993-Russell: ISESS’93 A Reality Check (DWR), pp. 637–640.
OOPSLA-1993-BruceCMGDM #decidability #object-oriented #type checking: Safe and Decidable Type Checking in an Object-Oriented Language (KBB, JC, TPM, RvG, AD, RM), pp. 29–46.
POPL-1993-Bruce #object-oriented #programming language #static typing #type checking: Safe Type Checking in a Statically-Typed Object-Oriented Programming Language (KBB), pp. 285–298.
POPL-1993-NipkowP #type checking: Type Checking Type Classes (TN, CP), pp. 409–418.
SAC-1993-Chen #fault #probability #robust: Effect of Probabilistic Error Checking Procedures and Performability of Robust Objects (IRC), pp. 677–681.
SOSP-1993-PerlW #performance: Performance Assertion Checking (SEP, WEW), pp. 134–145.
CAV-1993-ClarkeFJ #logic #model checking #symmetry: Exploiting Symmetry In Temporal Logic Model Checking (EMC, TF, SJ), pp. 450–462.
CAV-1993-DamsGG #generative #modelling: Generation of Reduced Models for Checking Fragments of CTL (DD, OG, RG), pp. 479–490.
CAV-1993-EmersonJS #calculus #model checking #on the #μ-calculus: On Model-Checking for Fragments of μ-Calculus (EAE, CSJ, APS), pp. 385–396.
CAV-1993-EmersonS #model checking #symmetry: Symmetry and Model Checking (EAE, APS), pp. 463–478.
CAV-1993-FernandezKM #equivalence: Symbolic Equivalence Checking (JCF, AK, LM), pp. 85–96.
CAV-1993-Hungar #model checking #parallel #process #proving #theorem proving #verification: Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.
CAV-1993-Peled #model checking #using: All from One, One for All: on Model Checking Using Representatives (DP), pp. 409–423.
ISSTA-1993-Blum #design #source code: Designing Programs to Check Their Work (Abstract) (MB), p. 1.
DAC-1992-Peltz #design #interpreter: An Interpreter for General Netlist Design Rule Checking (GP), pp. 305–310.
ESOP-1992-Andersen #graph #model checking: Model Checking and Boolean Graphs (HRA), pp. 1–19.
ICALP-1992-Rabinovich #concurrent #finite: Checking Equivalences Between Concurrent Systems of Finite Agents (Extended Abstract) (AMR), pp. 696–707.
CIKM-1992-MartinAD #approach #behaviour #consistency #database #object-oriented: Consistency Checking in Object Oriented Databases: a Behavioral Approach (HM, MEA, BD), pp. 53–68.
SEKE-1992-HaoTJ #consistency #modelling #nondeterminism #process #prototype: Prototyping an Inconsistency Checking Tool for Software Process Models (JKH, FT, JJ), pp. 227–234.
PLILP-1992-AptP #problem #why: Why the Occur-Check is Not a Problem (KRA, AP), pp. 69–86.
PLILP-1992-SaidiB #debugging #two-level grammar: Checking and Debugging of Two-level Grammars (SS, JFB), pp. 158–171.
POPL-1992-ClarkeGL #abstraction #model checking: Model Checking and Abstraction (EMC, OG, DEL), pp. 342–354.
ICSE-1992-FelderM #realtime #specification #validation: Validating Real-Time Systems by History-Checking TRIO Specifications (MF, AM), pp. 199–211.
SOSP-WIP-1991-Perl92 #performance: Performance Assertion Checking (Abstract) (SEP), p. 25.
CAV-1992-Bradfield #model checking #proving: A Proof Assistant for Symbolic Model-Checking (JCB), pp. 316–329.
CAV-1992-CleavelandKS #calculus #model checking #performance #μ-calculus: Faster Model Checking for the Modal μ-Calculus (RC, MK, BS), pp. 410–422.
CAV-1992-Kaivola #composition #linear #logic #model checking: Compositional Model Checking for Linear-Time Temporal Logic (RK), pp. 248–259.
CAV-1992-Larsen #correctness #performance: Efficient Local Correctness Checking (KGL), pp. 30–43.
CAV-1992-RicoBC #model checking #realtime: Model-Checking for Real-Time Systems Specified in Lotos (NR, GvB, OC), pp. 288–301.
CAV-1992-ShipleCSB #automation #composition #model checking #reduction: Automatic Reduction in CTL Compositional Model Checking (TRS, MC, ALSV, RKB), pp. 234–247.
JICSLP-1992-Dumant: Checking the Soundness of Resolution Schemes (BD), pp. 37–51.
LICS-1992-HenzingerNSY #model checking #realtime: Symbolic Model Checking for Real-time Systems (TAH, XN, JS, SY), pp. 394–406.
DAC-1991-BurchCL #model checking #representation: Representing Circuits More Efficiently in Symbolic Model Checking (JRB, EMC, DEL), pp. 403–407.
STOC-1991-BabaiFLS: Checking Computations in Polylogarithmic Time (LB, LF, LAL, MS), pp. 21–31.
WSA-1991-BoeckC #analysis #automation #prolog #type checking: Automatic Construction of Prolog Primitives for Type Checking Analysis (PDB, BLC), pp. 165–172.
ICALP-1991-AlurCD #model checking #probability #realtime: Model-Checking for Probabilistic Real-Time Systems (Extended Abstract) (RA, CC, DLD), pp. 115–126.
VDME-1991-1-DammHB #consistency #on the #type checking: On Type Checking in VDM and Related Consistency Issues (FMD, BSH, HB), pp. 45–62.
KR-1991-HalpernV #model checking #proving #theorem proving: Model Checking vs. Theorem Proving: A Manifesto (JYH, MYV), pp. 325–334.
OOPSLA-1991-AgrawalDL #multi #static typing #type checking: Static Type Checking of Multi-Methods (RA, LGD, BGL), pp. 113–128.
LOPSTR-1991-Lever #development #equivalence: Program Equivalence, Program Development and Integrity Checking (JML), pp. 1–12.
PLILP-1991-FileS #abstract interpretation #type checking: Abstract Interpretation for Type Checking (GF, PS), pp. 311–322.
CAV-1991-AndersenW #composition: Compositional Checking of Satisfaction (HRA, GW), pp. 24–36.
CAV-1991-BevierS #kernel #proving #specification: Mechanically Checked Proofs of Kernel Specification (WRB, JFSA), pp. 70–82.
CAV-1991-CleavelandS #algorithm #calculus #linear #model checking #μ-calculus: A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal μ-Calculus (RC, BS), pp. 48–58.
CAV-1991-DillHW #simulation #using: Checking for Language Inclusion Using Simulation Preorders (DLD, AJH, HWT), pp. 255–265.
CAV-1991-EndersFT #generative #model checking: Generating BDDs for Symbolic Model Checking in CCS (RE, TF, DT), pp. 203–213.
CAV-1991-Filkorn #functional #model checking: Functional Extension of Symbolic Model Checking (TF), pp. 225–232.
CAV-1991-FrancescoI #process #semantics: A Semantic Driven Method to Check the Finiteness of CCS Processes (NDF, PI), pp. 266–276.
CAV-1991-HamaguchiHY #branch #logic #model checking #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 #model checking #verification: Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification (HH, KH, HO, SY), pp. 214–224.
CAV-1991-ProbstL #model checking #partial order: Partial-Order Model Checking: A Guide for the Perplexed (DKP, HFL), pp. 322–331.
CSL-1991-BestE #model checking #persistent #petri net: Model Checking of Persistent Petri Nets (EB, JE), pp. 35–52.
ISLP-1991-DeransartFT #source code: NSTO Programs (Not Subject to Occur-Check) (PD, GF, MT), pp. 533–547.
IWPTS-1991-Petrenko #protocol: Checking Experiments with Protocol Machines (AP), pp. 83–94.
LICS-1991-GodefroidW #approach #model checking: A Partial Approach to Model Checking (PG, PW), pp. 406–415.
TAV-1991-Sankar #algebra #consistency #runtime #specification: Run-Time Consistency Checking of Algebraic Specifications (SS), pp. 123–129.
DAC-1990-BurchCMD #model checking #using #verification: Sequential Circuit Verification Using Symbolic Model Checking (JRB, EMC, KLM, DLD), pp. 46–51.
DAC-1990-SuzukiO #design #online: A Practical Online Design Rule Checking System (GS, YO), pp. 246–252.
PLDI-1990-Gupta #array #bound #fresh look #optimisation: A Fresh Look at Optimizing Array Bound Checking (RG), pp. 272–282.
VDME-1990-PlatHKOPT #type checking: Type Checking BSI/VDM-SL (NP, RH, JvK, GvO, KP, HT), pp. 399–425.
CAV-1990-CamuratiGPR #model checking: The Use of Model Checking in ATPG for Sequential Circuits (PC, MG, PP, MSR), pp. 86–95.
CAV-1990-Clarke #explosion #logic #model checking #problem: Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem (EMC), p. 1.
CAV-1990-HamaguchiHY #branch #complexity #linear #logic #model checking: Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity (KH, HH, SY), pp. 253–262.
CAV-1990-HiraishiMH #logic #model checking: Vectorized Model Checking for Computation Tree Logic (HH, SM, KH), pp. 44–53.
CLP-1990-GriefahnL90 #constraints #database #deduction #top-down: Top-Down Integrity Constraint Checking for Deductive Databases (UG, SL), pp. 130–144.
LICS-1990-AlurCD #model checking #realtime: Model-Checking for Real-Time Systems (RA, CC, DLD), pp. 414–425.
LICS-1990-BurchCMDH #model checking: Symbolic Model Checking: 10^20 States and Beyond (JRB, EMC, KLM, DLD, LJH), pp. 428–439.
NACLP-1990-Bol #performance #towards: Towards More Efficient Loop Checks (RNB), pp. 465–479.
DAC-1989-BonapaceL #algorithm #design: An O(nlogm) Algorithm for VLSI Design Rule Checking (CRB, CYL), pp. 503–507.
DAC-1989-Ghewala #named #testing: CrossCheck: A Cell Based VLSI Testability Solution (TG), pp. 706–709.
DAC-1989-HedenstiernaJ #design #layout: The Use of Inverse Layout Trees for Hierarchical Design Rule Checking (NH, KOJ), pp. 508–512.
HT-1989-EhrmannEMW #education #hypermedia: Hypertext and Higher Education: A Reality Check (SCE, SE, KM, RFEW), p. 393.
SIGMOD-1989-CammarataRS #database #relational: Extendeing a Relational Database with Deferred Referential Integrity Checking and Intelligent Joins (SJC, PR, DS), pp. 88–97.
STOC-1989-BlumK #design #source code: Designing Programs That Check Their Work (MB, SK), pp. 86–97.
ICALP-1989-Winskel #calculus #model checking: A Note on Model Checking the Modal nu-Calculus (GW), pp. 761–772.
LICS-1989-ClarkeLM #composition #model checking: Compositional Model Checking (EMC, DEL, KLM), pp. 353–362.
DAC-1988-TakashimaIKTSS #comparison #functional #morphism #rule-based: A Circuit Comparison System with Rule-Based Functional Isomorphism Checking (MT, AI, SK, TT, TS, JiS), pp. 512–516.
ICALP-1988-Weijland #logic programming #semantics #source code: Semantics for Logic Programs without Occur Check (WPW), pp. 710–726.
PLILP-1988-BarbutiM #logic programming #source code: A Tool to Check the Non-Floundering Logic Programs and Goals (RB, MM), pp. 58–67.
CCHSC-1988-Levy #in the large #type checking: Type Checking in the Large (MRL), pp. 137–145.
CADE-1988-Simon #natural language #proving: Checking Natural Language Proofs (DS), pp. 141–150.
VLDB-1987-KowalskiSS #database #deduction: Integrity Checking in Deductive Databases (RAK, FS, PS), pp. 61–69.
OOPSLA-1987-Thorelli #ll #type checking: Modules and Type Checking in PL/LL (LET), pp. 268–276.
ASPLOS-1987-SteenkisteH #hardware #lisp #type checking: Tags and Type Checking in Lisp: Hardware and Software Approaches (PS, JLH), pp. 50–59.
ICLP-1987-HentenryckD87 #logic programming: Forward Checking in Logic Programming (PVH, MD), pp. 229–256.
VLDB-1986-BryM #consistency #constraints #database #logic: Checking Consistency of Database Constraints: a Logical Basis (FB, RM), pp. 13–20.
ESOP-1986-Sondergaard #abstract interpretation #logic programming #reduction #source code: An Application of Abstract Interpretation of Logic Programs: Occur Check Reduction (HS), pp. 327–338.
OOPSLA-1986-Johnson #smalltalk: Type-Checking Smalltalk (REJ), pp. 315–321.
LICS-1986-EmersonL #calculus #model checking #performance #μ-calculus: Efficient Model Checking in Fragments of the Propositional μ-Calculus (Extended Abstract) (EAE, CLL), pp. 267–278.
DAC-1985-BierP #algorithm #design #multi: An algorithm for design rule checking on a multiprocessor (GEB, ARP), pp. 299–304.
SIGMOD-1985-HsuI #multi: Integrity Checking for Multiple Updates (AH, TI), pp. 152–168.
POPL-1985-EmersonL #branch #model checking: Modalities for Model Checking: Branching Time Strikes Back (EAE, CLL), pp. 84–96.
POPL-1985-LichtensteinP #concurrent #finite #linear #source code #specification: Checking That Finite State Concurrent Programs Satisfy Their Linear Specification (OL, AP), pp. 97–107.
POPL-1985-MishraR #type checking: Declaration-Free Type Checking (PM, USR), pp. 7–21.
DAC-1984-ChapmanC #approach #case study #design #experience: The scan line approach to design rules checking: Computational experiences (PTC, KCJ), pp. 235–241.
VLDB-1984-Tan #constraints #dependence: A Less Costly Constraints Checking for Join Dependency (KPT), pp. 63–68.
SCC-1984-BaiardiRV #communication #static analysis: Static checking of interprocess communication in ECSP (FB, LR, MV), pp. 290–299.
SCC-1984-Levy #compilation #reuse #type checking: Type checking, separate compilation and reusability (MRL), pp. 285–289.
LFP-1984-Katayama #approach #functional #programming language #type checking #type inference: Type Inference and Type Checking for Functional Programming Languages: A Reduced Computation Approach (TK), pp. 263–272.
POPL-1984-RepsA #interactive #proving: Interactive Proof Checking (TWR, BA), pp. 36–45.
SLP-1984-Plaisted84 #problem #prolog: The Occur-Check Problem in Prolog (DAP), pp. 272–280.
DAC-1983-Bhavsar #algorithm #calculus #design: Design For Test Calculus: An algorithm for DFT rules checking (DKB), pp. 300–307.
DAC-1983-ChangA #consistency: Consistency checking for MOS/VLSI circuits (NSC, RA), pp. 732–733.
POPL-1983-Meertens #incremental #polymorphism #type checking: Incremental Polymorphic Type Checking in B (LGLTM), pp. 265–275.
DAC-1982-ArnoldO #approach #geometry #layout #named: Lyra: A new approach to geometric layout rule checking (MHA, JKO), pp. 530–536.
DAC-1982-EustaceM #approach #automaton #design #finite: A Deterministic finite automaton approach to design rule checking for VLSI (RAE, AM), pp. 712–717.
DAC-1982-Seiler #architecture #design #hardware: A hardware assisted design rule check architecture (LS), pp. 232–238.
VLDB-1982-Lafue #dependence #semantics: Semantic Integrity Dependencies and Delayed Integrity Checking (GMEL), pp. 292–299.
SCC-1982-MarksteinCM #optimisation: Optimization of Range Checking (VM, JC, PWM), pp. 114–119.
Best-of-PLDI-1982-MarksteinMC #optimisation: Optimization of range checking (with retrospective) (VM, PWM, JC), pp. 58–65.
ICSE-1982-RudmikCC #consistency #design #embedded: Consistency Checking within Embedded Design Languages (AR, BEC, HC), pp. 236–245.
DAC-1981-Corbin: Custom VLSI electrical rule checking in an intelligent terminal (LVC), pp. 696–701.
DAC-1981-KamikawaiYCFT: A critical path delay check system (RK, MY, TC, KF, YT), pp. 118–123.
DAC-1980-ChaoHY #approach #consistency #layout: A hierarchical approach for layout versus circuit consistency check (SPC, YSH, LMY), p. 269.
DAC-1980-ChaoHY80a #approach #consistency #layout: A hierarchical approach for layout versus circuit consistency check (SPC, YSH, LMY), pp. 270–276.
DAC-1980-McGrathW #design #layout #verification: Design integrity and immunity checking: A new look at layout verification and design rule checking (EJM, TW), pp. 263–268.
VLDB-1980-Wilson #concept #semantics: A Conceptual Model for Semantic Integrity Checking (GAW), pp. 111–125.
POPL-1980-DemersD #data type #parametricity #type checking: Data Types, Parameters, and Type Checking (AJD, JED), pp. 12–23.
DAC-1979-BennettSC #design #editing #interactive: Dynamic design rule checking in an interactive printed circuit editor (TCB, KRS, WMvC), pp. 330–336.
DAC-1979-Chang #layout #recognition #using: LSI layout checking using bipolar device recognition technique (CSC), pp. 95–101.
DAC-1979-McCaw: Unified Shapes Checker — a checking tool for LSI (CRM), pp. 81–87.
DAC-1979-Preiss #2d #3d #consistency #finite: A procedure for checking the topological consistency of a 2-D or 3-D finite element mesh (KP), pp. 200–206.
VLDB-1979-Demolombe #calculus #semantics: Semantic Checking of Questions Expressed in Predicate Calculus Language (RD), pp. 444–450.
SCC-1979-Williams: Program checking (GW), pp. 13–25.
POPL-1979-Miller #type checking: Type Checking in an Imperfect World (TCM), pp. 237–243.
POPL-1978-DemersDS #data type #encapsulation #morphism #polymorphism: Data Types as Values: Polymorphism, Type-Checking, Encapsulation (AJD, JED, GS), pp. 23–30.
ICSE-1978-KieburtzBH #pascal: A Type-Checking Program Linkage System for Pascal (RBK, WB, CRH), pp. 23–28.
DAC-1977-GodoyFB #automation #design #logic #testing: Automatic checking of logic design structures For compliance with testability ground rules (HCG, GBF, PSB), pp. 469–478.
DAC-1977-YoshidaMNCON #layout #scalability: A layout checking system for large scale integrated circuits (KY, TM, YN, TC, KO, SN), pp. 322–330.
DAC-1976-BuntineP #analysis #design: Design rule checking and analysis of IC mask designs (WLB, BP), pp. 301–308.
DAC-1976-IkemotoSIK: Correction and wiring check-system for master-slice LSI (YI, TS, KI, HK), pp. 336–343.
DAC-1976-PiscatelliT: A solution to closeness checking of non-orthogonal printed circuit board wiring (RNP, PT), pp. 172–178.
DIPL-1976-Brosgol #data type #type checking: Some issues in data types and type checking (BMB), pp. 102–130.
DIPL-1976-FischerL #data access #runtime: Run-time checking of data access in Pascal-like languages (CNF, RJL), pp. 215–230.
DAC-1974-RosenbergB #design #named: CRITIC — an integrated circuit design rule checking program (LMR, CB), pp. 14–18.
ICALP-1974-ShamirB: Checking Stacks and Context-Free Programmed Grammars Accept p-complete Languages (ES, CB), pp. 27–33.
DAC-1972-ChangDE #analysis #fault #logic #self #simulation: Logic simulation and fault analysis of a self-checking switching processor (HYC, RCD, RAE), pp. 128–137.
DAC-1970-Koga: A checking method of wiring (YK), pp. 173–177.