BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Used together with:
model (1017)
system (196)
use (190)
base (160)
program (134)

Stem check$ (all stems)

1725 papers:

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

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