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:
system (84)
use (80)
program (80)
model (57)
properti (49)

Stem verifi$ (all stems)

556 papers:

CASECASE-2015-AicherRV #abstraction #automation #simulation #towards #verification
Towards finding the appropriate level of abstraction to model and verify automated production systems in discrete event simulation (TA, SR, BVH), pp. 1048–1053.
DACDAC-2015-AsadJ #programming #using #verification
Verifying inevitability of phase-locking in a charge pump phase lock loop using sum of squares programming (HuA, KDJ), p. 6.
DACDAC-2015-HerdtLD #simulation #using #verification
Verifying SystemC using stateful symbolic simulation (VH, HML, RD), p. 6.
DATEDATE-2015-MadhukarSWKM #abstraction #lazy evaluation #using #verification
Verifying synchronous reactive systems using lazy abstraction (KM, MS, BW, DK, RM), pp. 1571–1574.
ESOPESOP-2015-EberlHN #compilation #probability
A Verified Compiler for Probability Density Functions (ME, JH, TN), pp. 80–104.
ESOPESOP-2015-SergeyNB #algorithm #concurrent #specification #verification
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity (IS, AN, AB), pp. 333–358.
FASEFASE-2015-CzechJW #exclamation #verification #what
Just Test What You Cannot Verify! (MC, MCJ, HW), pp. 100–114.
TACASTACAS-2015-Beyer #verification
Software Verification and Verifiable Witnesses — (Report on SV-COMP 2015) (DB), pp. 401–416.
TACASTACAS-2015-ChenHTWW #contest #named #program transformation #recursion #source code #text-to-text #verification
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation — (Competition Contribution) (YFC, CH, MHT, BYW, FW), pp. 426–428.
TACASTACAS-2015-GurfinkelKN #c #contest #framework #named #source code #verification
SeaHorn: A Framework for Verifying C Programs (Competition Contribution) (AG, TK, JAN), pp. 447–450.
TACASTACAS-2015-HaranCELQR #composition #contest #verification
SMACK+Corral: A Modular Verifier — (Competition Contribution) (AH, MC, ME, AL, SQ, ZR), pp. 451–454.
TACASTACAS-2015-Immler #analysis #reachability
Verified Reachability Analysis of Continuous Systems (FI), pp. 37–51.
TACASTACAS-2015-JeanninGKGSZP #hybrid
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System (JBJ, KG, YK, RG, AS, EZ, AP), pp. 21–36.
TACASTACAS-2015-TomascoI0TP15a #concurrent #memory management #source code #verification
Verifying Concurrent Programs by Memory Unwinding (ET, OI, BF, SLT, GP), pp. 551–565.
PEPMPEPM-2015-AsadaS0 #first-order #functional #refinement #relational #source code #verification
Verifying Relational Properties of Functional Programs by First-Order Refinement (KA, RS, NK), pp. 61–72.
PLDIPLDI-2015-GammieHE #garbage collection #on the fly
Relaxing safely: verified on-the-fly garbage collection for x86-TSO (PG, ALH, KE), pp. 99–109.
PLDIPLDI-2015-TassarottiDV #logic #memory management #verification
Verifying read-copy-update in a logic for weak memory (JT, DD, VV), pp. 110–120.
PLDIPLDI-2015-WilcoxWPTWEA #distributed #framework #implementation #named #verification
Verdi: a framework for implementing and formally verifying distributed systems (JRW, DW, PP, ZT, XW, MDE, TEA), pp. 357–368.
FMFM-2015-BratBDGHK #safety #verification
Verifying the Safety of a Flight-Critical System (GB, DHB, MD, DG, FH, TK), pp. 308–324.
FMFM-2015-DerrickDSTW #transaction #verification
Verifying Opacity of a Transactional Mutex Lock (JD, BD, GS, OT, HW), pp. 161–177.
FMFM-2015-LiSLD #protocol #security #verification
Verifying Parameterized Timed Security Protocols (LL, JS, YL, JSD), pp. 342–359.
FMFM-2015-MirandaMR #automation #design #generative #testing #using #verification
Using Simulink Design Verifier for Automatic Generation of Requirements-Based Tests (BM, HM, RR), pp. 601–604.
FMFM-2015-PolikarpovaTF #library
A Fully Verified Container Library (NP, JT, CAF), pp. 414–434.
SEFMSEFM-2015-Muhlberg0DLP #learning #source code #verification
Learning Assertions to Verify Linked-List Programs (JTM, DHW, MD, GL, FP), pp. 37–52.
SEFMSEFM-2015-Vanspauwen0 #encryption #implementation #library #protocol #specification #verification
Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications (GV, BJ), pp. 53–68.
ICFPICFP-2015-NeisHKMDV #compilation #higher-order #imperative #named
Pilsner: a compositionally verified compiler for a higher-order imperative language (GN, CKH, JOK, CM, DD, VV), pp. 166–178.
ICGTICGT-2015-Stuckrath #analysis #graph transformation #named #using #verification
Uncover: Using Coverability Analysis for Verifying Graph Transformation Systems (JS), pp. 266–274.
SEKESEKE-2015-LiuH #petri net #pipes and filters #verification
PIPE+Verifier — A Tool for Analyzing High Level Petri Nets (SL, XH), pp. 575–580.
MoDELSMoDELS-2015-OakesTLW #atl #contract #declarative #verification
Fully verifying transformation contracts for declarative ATL (BJO, JT, LL, MW), pp. 256–265.
MoDELSMoDELS-2015-SongLASDC #architecture #formal method #probability #using #verification
Formalizing and verifying stochastic system architectures using Monterey Phoenix (SoSyM abstract) (SS, YL, MA, JS, JSD, TC), p. 449.
ECOOPECOOP-2015-SchwerhoffS #automation #lightweight #verification
Lightweight Support for Magic Wands in an Automatic Verifier (MS, AJS), pp. 614–638.
ECOOPECOOP-2015-VekrisCJ #trust #type system #verification
Trust, but Verify: Two-Phase Typing for Dynamic Languages (PV, BC, RJ), pp. 52–75.
OOPSLAOOPSLA-2015-BastaniAA #android #data flow #verification
Interactively verifying absence of explicit information flows in Android apps (OB, SA, AA), pp. 299–315.
OOPSLAOOPSLA-2015-WickersonBBD
Remote-scope promotion: clarified, rectified, and verified (JW, MB, BMB, AFD), pp. 731–747.
POPLPOPL-2015-JourdanLBLP #c
A Formally-Verified C Static Analyzer (JHJ, VL, SB, XL, DP), pp. 247–259.
SACSAC-2015-CostaCFR #diagrams #modelling #precise #uml
From UML diagrams to simulink models: a precise and verified translation (AC, SAdCC, LF, LR), pp. 1547–1552.
SACSAC-2015-KhelladiBBLG #consistency #framework #process #verification
A framework to formally verify conformance of a software process to a software method (DEK, RB, SB, YL, MPG), pp. 1518–1525.
SACSAC-2015-LeTN #requirements #using #verification
Verifying eventuality properties of imprecise system requirements using event-B (HAL, NTT, SN), pp. 1651–1653.
ESEC-FSEESEC-FSE-2015-0001DDHS #validation #verification
Witness validation and stepwise testification across software verifiers (DB, MD, DD, MH, AS), pp. 721–733.
ICSEICSE-v1-2015-JoblinMASR #approach #community #developer #fine-grained #network
From Developer Networks to Verified Communities: A Fine-Grained Approach (MJ, WM, SA, JS, DR), pp. 563–573.
CCCC-2015-DemangePS #coq #optimisation #performance #verification
Verifying Fast and Sparse SSA-Based Optimizations in Coq (DD, DP, LS), pp. 233–252.
LCTESLCTES-2015-LinM #distributed #framework #named #programming #simulation #towards #verification
StarL: Towards a Unified Framework for Programming, Simulating and Verifying Distributed Robotic Systems (YL, SM), p. 10.
CAVCAV-2015-Leslie-HurdCF #verification
Verifying Linearizability of Intel® Software Guard Extensions (RLH, DC, MF), pp. 144–160.
ICSTICST-2015-KobashiYWFYOK #design pattern #named #security #testing #verification
TESEM: A Tool for Verifying Security Design Pattern Applications by Model Testing (TK, MY, HW, YF, NY, TO, HK), pp. 1–8.
ICSTICST-2015-ZhangAC #exclamation #model checking #verification
Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications (HZ, TA, YC), pp. 1–10.
TAPTAP-2015-MoreiraHDMNM #case study #code generation #testing #tool support #using #verification
Verifying Code Generation Tools for the B-Method Using Tests: A Case Study (AMM, CH, DD, ECBdM, JBSN, VdMJ), pp. 76–91.
QoSAQoSA-2014-Meyer #question #trust #verification
Trust or verify? (BM), pp. 1–2.
ASEASE-2014-UbayashiALLHK #compilation #verification
Abstraction-aware verifying compiler for yet another MDD (NU, DA, PL, YNL, SH, YK), pp. 557–562.
ASEASE-2014-YangXLCML #adaptation #nondeterminism #self #verification
Verifying self-adaptive applications suffering uncertainty (WY, CX, YL, CC, XM, JL), pp. 199–210.
DACDAC-2014-SorinMZ #architecture #power management
Architecting Dynamic Power Management to be Formally Verifiable (DJS, OM, MZ), p. 3.
DATEDATE-2014-LeD #design #towards #verification
Towards verifying determinism of SystemC designs (HML, RD), pp. 1–4.
ESOPESOP-2014-BeringerSDA #c #compilation
Verified Compilation for Shared-Memory C (LB, GS, RD, AWA), pp. 107–127.
ESOPESOP-2014-PercontiA #compilation #multi #semantics #using #verification
Verifying an Open Compiler Using Multi-language Semantics (JTP, AA), pp. 128–148.
FASEFASE-2014-Zaharieva-StojanovskiH #concurrent #invariant #source code #verification
Verifying Class Invariants in Concurrent Programs (MZS, MH), pp. 230–245.
TACASTACAS-2014-AngelisFPP #named #source code #verification
VeriMAP: A Tool for Verifying Programs through Transformations (EDA, FF, AP, MP), pp. 568–574.
WRLAWRLA-2014-BartolettiMSZ #maude #modelling #verification
Modelling and Verifying Contract-Oriented Systems in Maude (MB, MM, AS, RZ), pp. 130–146.
SANERCSMR-WCRE-2014-MihanceaM #named #security #verification #web
JMODEX: Model extraction for verifying security properties of web applications (PFM, MM), pp. 450–453.
PEPMPEPM-2014-CosteaSD #named #verification
HIPimm: verifying granular immutability guarantees (AC, AS, CD), pp. 189–194.
PLDIPLDI-2014-BallBGIKSSV #named #network #source code #towards #verification
VeriCon: towards verifying controller programs in software-defined networks (TB, NB, AG, SI, AK, MS, MS, AV), p. 31.
PLDIPLDI-2014-JagannathanPVPL #compilation #refinement
Atomicity refinement for verified compilation (SJ, GP, JV, DP, VL), p. 5.
PLDIPLDI-2014-SampsonPMMGC #probability #verification
Expressing and verifying probabilistic assertions (AS, PP, TM, KSM, DG, LC), p. 14.
SASSAS-2014-ChenHTWW #recursion #source code #using #verification
Verifying Recursive Programs Using Intraprocedural Analyzers (YFC, CH, MHT, BYW, FW), pp. 118–133.
DLTDLT-2014-YakaryilmazSD #quantum #verification
Debates with Small Transparent Quantum Verifiers (AY, ACCS, HGD), pp. 327–338.
ICALPICALP-v1-2014-Kuncak #recursion #verification
Verifying and Synthesizing Software with Recursive Functions — (Invited Contribution) (VK), pp. 11–25.
FMFM-2014-ChristakisLS #formal method #verification
Formalizing and Verifying a Modern Build Language (MC, KRML, WS), pp. 643–657.
FMFM-2014-DerrickDSTTW #consistency #verification
Quiescent Consistency: Defining and Verifying Relaxed Linearizability (JD, BD, GS, BT, OT, HW), pp. 200–214.
FMFM-2014-GuptaKG #experience #verification
Formally Verifying Graphics FPU — An Intel® Experience (AG, VMAK, RG), pp. 673–687.
FMFM-2014-LeinoM #automation #induction #proving #verification
Co-induction Simply — Automatic Co-inductive Proofs in a Program Verifier (KRML, MM), pp. 382–398.
IFMIFM-2014-BrideKP #constraints #specification #theorem proving #using #verification #workflow
Verifying Modal Workflow Specifications Using Constraint Solving (HB, OK, FP), pp. 171–186.
IFMIFM-2014-DerrickSD #architecture #verification
Verifying Linearizability on TSO Architectures (JD, GS, BD), pp. 341–356.
IFMIFM-2014-MellerGY #behaviour #uml #verification
Verifying Behavioral UML Systems via CEGAR (YM, OG, KY), pp. 139–154.
SEFMSEFM-2014-DiagneMF #verification
A Tool for Verifying Dynamic Properties in B (FD, AM, MF), pp. 290–295.
SEFMSEFM-2014-DuboisR #functional #using
Verified Functional Iterators Using the FoCaLiZe Environment (CD, RR), pp. 317–331.
ICGTICGT-2014-PoskittP #graph #higher-order #monad #source code #verification
Verifying Monadic Second-Order Properties of Graph Programs (CMP, DP), pp. 33–48.
HILTHILT-2014-BocchinoGGS #named #programming language
Spot: a programming language for verified flight software (RLB, EG, KPG, RRS), pp. 97–102.
CIKMCIKM-2014-CalvaneseMET #modelling #process #uml
Verifiable UML Artifact-Centric Business Process Models (DC, MM, ME, ET), pp. 1289–1298.
SEKESEKE-2014-GuimaraesSALC #alloy #consistency #using #verification
A Method for Verifying the Consistency of Business Rules Using Alloy (DG, EAS, AJA, PL, ALC), pp. 381–386.
AMTAMT-2014-ZhangBBEHKW #code generation #concurrent #java #state machine #towards
Towards Verified Java Code Generation from Concurrent State Machines (DZ, DB, MvdB, LE, CH, RK, AW), pp. 64–69.
MODELSMoDELS-2014-ChakiE #compilation #distributed #modelling #verification
Model-Driven Verifying Compilation of Synchronous Distributed Applications (SC, JRE), pp. 201–217.
MODELSMoDELS-2014-ChakiE #compilation #distributed #modelling #verification
Model-Driven Verifying Compilation of Synchronous Distributed Applications (SC, JRE), pp. 201–217.
POPLPOPL-2014-AmorimCDDHPPPT #architecture #data flow
A verified information-flow architecture (AAdA, NC, AD, DD, CH, DP, BCP, RP, AT), pp. 165–178.
POPLPOPL-2014-BouajjaniEH #consistency #replication #verification
Verifying eventual consistency of optimistic replication systems (AB, CE, JH), pp. 285–296.
POPLPOPL-2014-KumarMNO #implementation #ml #named
CakeML: a verified implementation of ML (RK, MOM, MN, SO), pp. 179–192.
FSEFSE-2014-LalQ #using #verification
Powering the static driver verifier using corral (AL, SQ), pp. 202–212.
FSEFSE-2014-VakiliD #infinity #modelling #smt #using #verification
Verifying CTL-live properties of infinite state models using an SMT solver (AV, NAD), pp. 213–223.
ICSEICSE-2014-MaozRR #component #modelling #verification
Verifying component and connector models against crosscutting structural views (SM, JOR, BR), pp. 95–105.
HPCAHPCA-2014-MatthewsZS #power management
Scalably verifiable dynamic power management (OM, MZ, DJS), pp. 579–590.
CAVCAV-2014-BinghamL #bound #fault #simulation #using #verification
Verifying Relative Error Bounds Using Symbolic Simulation (JB, JLH), pp. 277–292.
CAVCAV-2014-CimattiGMT #hybrid #ltl #verification
Verifying LTL Properties of Hybrid Systems with K-Liveness (AC, AG, SM, ST), pp. 424–440.
CAVCAV-2014-FerraraMNP #data access #named #policy #verification
Vac — Verifier of Administrative Role-Based Access Control Policies (ALF, PM, TLN, GP), pp. 184–191.
CAVCAV-2014-KanavL0 #documentation
A Conference Management System with Verified Document Confidentiality (SK, PL, AP), pp. 167–183.
CAVCAV-2014-RakamaricE #implementation #named #verification
SMACK: Decoupling Source Language Details from Verifier Implementations (ZR, ME), pp. 106–113.
ISSTAISSTA-2014-ShachamYGABSV #independence #verification
Verifying atomicity via data independence (OS, EY, GGG, AA, NGB, MS, MTV), pp. 26–36.
VMCAIVMCAI-2014-AngelisFPP #array #source code #verification
Verifying Array Programs by Transforming Verification Conditions (EDA, FF, AP, MP), pp. 182–202.
VMCAIVMCAI-2014-DragoiHVWZ #algorithm #framework #verification
A Logic-Based Framework for Verifying Consensus Algorithms (CD, TAH, HV, JW, DZ), pp. 161–181.
ASEASE-2013-CalinescuJR #self #verification
Developing self-verifying service-based systems (RC, KJ, YR), pp. 734–737.
DACDAC-2013-LeGHD #simulation #using #verification
Verifying SystemC using an intermediate verification language and symbolic simulation (HML, DG, VH, RD), p. 6.
DATEDATE-2013-AbdullaDRSZ #hybrid #liveness #memory management #safety #transaction #verification
Verifying safety and liveness for the FlexTM hybrid transactional memory (PAA, SD, AR, AS, YZ), pp. 785–790.
PODSPODS-2013-AbouziedAPHS #learning #quantifier #query #verification
Learning and verifying quantified boolean queries by example (AA, DA, CHP, JMH, AS), pp. 49–60.
ESOPESOP-2013-BouajjaniEEH #concurrent #source code #specification #verification
Verifying Concurrent Programs against Sequential Specifications (AB, ME, CE, JH), pp. 290–309.
ESOPESOP-2013-GotsmanRY #algorithm #concurrent #memory management #verification
Verifying Concurrent Memory Reclamation Algorithms with Grace (AG, NR, HY), pp. 249–269.
FASEFASE-2013-GudemannPSD #framework #named #verification
VerChor: A Framework for Verifying Choreographies (MG, PP, GS, AD), pp. 226–230.
FASEFASE-2013-NordioCF #javascript #named #verification
Javanni: A Verifier for JavaScript (MN, CC, CAF), pp. 231–234.
TACASTACAS-2013-PopeeaR #concurrent #contest #multi #named #source code #thread #verification
Threader: A Verifier for Multi-threaded Programs — (Competition Contribution) (CP, AR), pp. 633–636.
PEPMPEPM-2013-AngelisFPP #source code #verification
Verifying programs via iterated specialization (EDA, FF, AP, MP), pp. 43–52.
PEPMPEPM-2013-CarbinKMR #approximate #program transformation
Verified integrity properties for safe approximate program transformations (MC, DK, SM, MCR), pp. 63–66.
PLDIPLDI-2013-GuhaRF #network
Machine-verified network controllers (AG, MR, NF), pp. 483–494.
PLDIPLDI-2013-SewellMK #kernel #validation
Translation validation for a verified OS kernel (TALS, MOM, GK), pp. 471–482.
PLDIPLDI-2013-SwamyWSCL #higher-order #monad #source code #verification
Verifying higher-order programs with the dijkstra monad (NS, JW, CS, JC, BL), pp. 387–398.
ICALPICALP-v2-2013-DemriDS #complexity #on the #verification
On the Complexity of Verifying Regular Properties on Flat Counter Systems, (SD, AKD, AS), pp. 162–173.
LATALATA-2013-Etessami #algorithm #infinity #probability #recursion #verification
Algorithms for Analyzing and Verifying Infinite-State Recursive Probabilistic Systems (KE), p. 12.
IFMIFM-2013-SavaryFL #bytecode #detection #modelling #testing #using #verification
Detecting Vulnerabilities in Java-Card Bytecode Verifiers Using Model-Based Testing (AS, MF, JLL), pp. 223–237.
SEFMSEFM-2013-AmanC #migration #realtime
Real-Time Migration Properties of rTiMo Verified in Uppaal (BA, GC), pp. 31–45.
SEFMSEFM-2013-OliveiraJW #csp #multi #protocol
A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP (MVMO, ISdMJ, JW), pp. 46–60.
SEFMSEFM-2013-SuryadevaraSMP #behaviour #using #verification
Verifying MARTE/CCSL Mode Behaviors Using UPPAAL (JS, CCS, FM, PP), pp. 1–15.
ICFPICFP-2013-Chlipala #generative #hoare #logic #metaprogramming #verification
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier (AC), pp. 391–402.
ICFPICFP-2013-TraytelN #regular expression #word
Verified decision procedures for MSO on words based on derivatives of regular expressions (DT, TN), pp. 3–12.
GCMGCM-J-2012-PoskittP #correctness #graph #source code #verification
Verifying Total Correctness of Graph Programs (CMP, DP).
CHICHI-2013-Egelman #exclamation #facebook #privacy #trade-off #verification
My profile is my password, verify me!: the privacy/convenience tradeoff of facebook connect (SE), pp. 2369–2378.
HCIHIMI-HSM-2013-KimKL #design #standard #verification
Designing and Verifying Application Schema by Applying Standard Element for Managing Ocean Observation Data (STK, LKK, TYL), pp. 110–115.
HILTHILT-2013-Taft13a #ada #parallel #programming #set
Bringing safe, dynamic parallel programming to the spark verifiable subset of ada (STT), pp. 37–40.
KDIRKDIR-KMIS-2013-AlwazaePK #classification #verification
Verifying the Usefulness of a Classification System of Best Practices (MMSA, EP, HK), pp. 405–412.
OOPSLAOOPSLA-2013-CarbinMR #hardware #reliability #source code #verification
Verifying quantitative reliability for programs that execute on unreliable hardware (MC, SM, MCR), pp. 33–52.
OOPSLAOOPSLA-2013-ShiBH #optimisation #using
Code optimizations using formally verified properties (YS, BB, GH), pp. 427–442.
SACSAC-2013-MartinaP #induction #multi #protocol #security #using #verification
Verifying multicast-based security protocols using the inductive method (JEM, LCP), pp. 1824–1829.
SACSAC-2013-MoriguchiW #interactive #reuse #source code
An interactive extension mechanism for reusing verified programs (SM, TW), pp. 1236–1243.
ICSEICSE-2013-Leino #source code
Developing verified programs with dafny (KRML), pp. 1488–1490.
ASPLOSASPLOS-2013-CuiHWY #execution #symbolic computation #using #verification
Verifying systems rules using rule-directed symbolic execution (HC, GH, JW, JY), pp. 329–342.
ASPLOSASPLOS-2013-MaiPXKM #invariant #security #verification
Verifying security invariants in ExpressOS (HM, EP, HX, STK, PM), pp. 293–304.
PLOSPLOS-2013-FernandezKKA #component #framework #towards
Towards a verified component platform (MF, IK, GK, JA), p. 7.
SOSPSOSP-2013-BraunFRSBW #verification
Verifying computations with state (BB, AJF, ZR, STVS, AJB, MW), pp. 341–357.
CADECADE-2013-HeuleHW #verification
Verifying Refutations with Extended Resolution (MH, WAHJ, NW), pp. 345–359.
CAVCAV-2013-EsparzaLNNSS #execution #ltl #model checking
A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.
DATEDATE-2012-NarayananDZT #design #using #verification
Verifying jitter in an analog and mixed signal design using dynamic time warping (RN, AD, MHZ, ST), pp. 1413–1416.
DATEDATE-2012-RajeevMR #architecture #constraints #distributed #embedded #verification
Verifying timing synchronization constraints in distributed embedded architectures (ACR, SM, SR), pp. 200–205.
DATEDATE-2012-YipHI #3d #challenge #design #verification
Challenges in verifying an integrated 3D design (TGY, CYH, VI), pp. 167–168.
ESOPESOP-2012-BartheDP
A Formally Verified SSA-Based Middle-End — Static Single Assignment Meets CompCert (GB, DD, DP), pp. 47–66.
FASEFASE-2012-AlbertBGHR #source code
Verified Resource Guarantees for Heap Manipulating Programs (EA, RB, SG, RH, GRD), pp. 130–145.
FASEFASE-2012-HatvaniPS #adaptation #automaton #embedded #framework #verification
Adaptive Task Automata: A Framework for Verifying Adaptive Embedded Systems (LH, PP, CCS), pp. 115–129.
TACASTACAS-2012-BaslerDKKTW #c #contest #named #source code #verification
satabs: A Bit-Precise Verifier for C Programs — (Competition Contribution) (GB, AFD, AK, DK, MT, TW), pp. 552–555.
TACASTACAS-2012-GrebenshchikovGLPR #contest #horn clause #verification
HSF(C): A Software Verifier Based on Horn Clauses — (Competition Contribution) (SG, AG, NPL, CP, AR), pp. 549–551.
TACASTACAS-2012-HolzlN #model checking #verification
Verifying pCTL Model Checking (JH, TN), pp. 347–361.
SCAMSCAM-2012-Vidal #execution #symbolic computation #termination #verification
Closed Symbolic Execution for Verifying Program Termination (GV), pp. 34–43.
PLDIPLDI-2012-GrebenshchikovLPR #proving #verification
Synthesizing software verifiers from proof rules (SG, NPL, CP, AR), pp. 405–416.
PLDIPLDI-2012-LeungGAGJL #gpu #kernel #verification
Verifying GPU kernels by test amplification (AL, MG, YA, RG, RJ, SL), pp. 383–394.
FMFM-2012-GiorginoS #algorithm #correctness #pointer
Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction (MG, MS), pp. 202–216.
SEFMSEFM-2012-ZhuXMQQ #approach #concurrent #source code #verification
The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs (HZ, QX, CM, SQ, ZQ), pp. 172–187.
ICFPICFP-2012-StewartBA #proving #theorem proving
Verified heap theorem prover by paramodulation (GS, LB, AWA), pp. 3–14.
AdaEuropeAdaEurope-2012-FairbairnB #implementation #verification
Implementing and Verifying EDF Preemption-Level Resource Control (MLF, AB), pp. 193–206.
HILTHILT-2012-Leino #source code
Developing verified programs with Dafny (KRML), pp. 9–10.
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.
ICPRICPR-2012-TaniyamaH #image #recognition #robust
Robust car License Plate Recognition system verified with 163, 574 images captured in fields (KT, KH), pp. 1273–1276.
SEKESEKE-2012-CuiWLBZL #aspect-oriented #diagrams #petri net #process #verification
Verifying Aspect-Oriented Activity Diagrams Against Crosscutting Properties with Petri Net Analyzer (ZC, LW, XL, LB, JZ, XL), pp. 369–374.
MODELSMoDELS-2012-ButtnerEC #atl #off the shelf #on the #smt #using #verification
On Verifying ATL Transformations Using “off-the-shelf” SMT Solvers (FB, ME, JC), pp. 432–448.
MODELSMoDELS-2012-ButtnerEC #atl #off the shelf #on the #smt #using #verification
On Verifying ATL Transformations Using “off-the-shelf” SMT Solvers (FB, ME, JC), pp. 432–448.
OOPSLAOOPSLA-2012-BettsCDQT #gpu #kernel #named #verification
GPUVerify: a verifier for GPU kernels (AB, NC, AFD, SQ, PT), pp. 113–132.
OOPSLAOOPSLA-2012-LogozzoB #automation #composition #program repair
Modular and verified automatic program repair (FL, TB), pp. 133–146.
OOPSLAOOPSLA-2012-SchillerE #specification
Reducing the barriers to writing verified specifications (TWS, MDE), pp. 95–112.
POPLPOPL-2012-LiangFF #concurrent #program transformation #simulation #verification
A rely-guarantee-based simulation for verifying concurrent program transformations (HL, XF, MF), pp. 455–468.
POPLPOPL-2012-ZhaoNMZ #formal method #program transformation #representation
Formalizing the LLVM intermediate representation for verified program transformations (JZ, SN, MMKM, SZ), pp. 427–440.
SACSAC-2012-Affeldt #library #low level #on the
On construction of a library of formally verified low-level arithmetic functions (RA), pp. 1326–1331.
FSEFSE-2012-BeyerHKW #model checking #verification
Conditional model checking: a technique to pass information between verifiers (DB, TAH, MEK, PW), p. 57.
ICSEICSE-2012-AlkhalafBG #analysis #string #using #validation #verification
Verifying client-side input validation functions using string analysis (MA, TB, JLG), pp. 947–957.
ICSEICSE-2012-CookHSS #compilation #composition #specification #using #verification
Specification engineering and modular verification using a web-integrated verifying compiler (CTC, HKH, HS, MS), pp. 1379–1382.
ICSEICSE-2012-LutzLLKHMS #programmable #requirements #self #verification
Engineering and verifying requirements for programmable self-assembling nanomachines (RRL, JHL, JIL, TK, EH, DM, DAS), pp. 1361–1364.
OSDIOSDI-2012-Kapritsos0QCAD #all about #manycore #replication
All about Eve: Execute-Verify Replication for Multi-Core Servers (MK, YW, VQ, AC, LA, MD), pp. 237–250.
CAVCAV-2012-RondonBKJ #c #named #verification
CSolve: Verifying C with Liquid Types (PMR, AB, MK, RJ), pp. 744–750.
ICLPICLP-2012-SchandaB #development #programming #set #using
Using Answer Set Programming in the Development of Verified Software (FS, MB), pp. 72–85.
ICSTICST-2012-MeszarosL #graph transformation
Verified Operational Patterns with Graph Transformation (TM, TL), pp. 954–961.
ICSTICST-2012-SalayCG #towards #verification
Towards a Methodology for Verifying Partial Model Refinements (RS, MC, JG), pp. 938–945.
TAPTAP-2012-CarlierDG #constraints #design #testing
A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest (MC, CD, AG), pp. 35–50.
TAPTAP-2012-KiniryZH #consistency #library #specification #testing #verification
Testing Library Specifications by Verifying Conformance Tests (JRK, DMZ, RH), pp. 51–66.
VMCAIVMCAI-2012-CharltonHR #higher-order #named #source code #verification
Crowfoot: A Verifier for Higher-Order Store Programs (NC, BH, BR), pp. 136–151.
VMCAIVMCAI-2012-OeSOC #named #satisfiability
versat: A Verified Modern SAT Solver (DO, AS, CO, KC), pp. 363–378.
CBSECBSE-2011-BordeC #component #embedded #realtime #synthesis #towards
Towards verified synthesis of ProCom, a component model for real-time embedded systems (EB, JC), pp. 129–138.
ECSAECSA-2011-HamelGKBG #behaviour #transaction #verification
Verifying Composite Service Transactional Behavior with EVENT-B (LH, MG, MK, MTB, WG), pp. 67–74.
DATEDATE-2011-SoekenWD #aspect-oriented #modelling #uml #verification
Verifying dynamic aspects of UML models (MS, RW, RD), pp. 1077–1082.
VLDBVLDB-2012-CormodeTY11 #interactive #proving #streaming #verification
Verifying Computations with Streaming Interactive Proofs (GC, JT, KY), pp. 25–36.
ESOPESOP-2011-Appel
Verified Software Toolchain — (Invited Talk) (AWA), pp. 1–17.
PEPMPEPM-2011-AlbertBGHPR #using
Verified resource guarantees using COSTA and KeY (EA, RB, SG, RH, GP, GRD), pp. 73–76.
SASSAS-2011-VafeiadisN #optimisation #verification
Verifying Fence Elimination Optimisations (VV, FZN), pp. 146–162.
FMFM-2011-BartheBCL #verification
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization (GB, GB, JDC, CL), pp. 231–245.
FMFM-2011-BoyerGS #configuration management #protocol #specification #verification
Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP (FB, OG, GS), pp. 103–117.
FMFM-2011-DerrickSW #verification
Verifying Linearisability with Potential Linearisation Points (JD, GS, HW), pp. 323–337.
FMFM-2011-KlebanovMSLWAABCCHJLMPPRSTTUW #case study #contest #experience
The 1st Verified Software Competition: Experience Report (VK, PM, NS, GTL, VW, EA, RA, DB, RC, EC, MAH, BJ, KRML, RM, FP, NP, TR, JS, ST, TT, MU, BW), pp. 154–168.
FMFM-2011-LoosPN #adaptation #distributed #hybrid
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified (SML, AP, LN), pp. 42–56.
SEFMSEFM-2011-JacquelBDD #automation #proving #theorem proving #using #verification
Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (MJ, KB, DD, CD), pp. 253–268.
ICEISICEIS-v3-2011-LinLMZN #approach #verification #workflow
Approach for Verifying Workflow Validity (YL, TL, IM, RZ, RN), pp. 66–75.
KEODKEOD-2011-KhuratS #approach #ontology #policy #verification
An Ontological Approach to Verifying P3P Policies (AK, BS), pp. 349–353.
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.
ECOOPECOOP-2011-BalzerG #invariant #multi #verification
Verifying Multi-object Invariants with Relationships (SB, TRG), pp. 358–382.
GPCEGPCE-2011-SlattenKH #automation #case study #distributed #generative #industrial #reliability #specification #towards #validation #verification
Towards automatic generation of formal specifications to validate and verify reliable distributed systems: a method exemplified by an industrial case study (VS, FAK, PH), pp. 147–156.
POPLPOPL-2011-GuptaPR #abstraction #concurrent #multi #refinement #source code #thread #verification
Predicate abstraction and refinement for verifying multi-threaded programs (AG, CP, AR), pp. 331–344.
POPLPOPL-2011-Leroy #question #tool support
Verified squared: does critical software deserve verified tools? (XL), pp. 1–2.
POPLPOPL-2011-OngR #algebra #data type #functional #higher-order #pattern matching #source code #verification
Verifying higher-order functional programs with pattern-matching algebraic data types (CHLO, SJR), pp. 587–598.
POPLPOPL-2011-SevcikVNJS #compilation #concurrent
Relaxed-memory concurrency and verified compilation (JS, VV, FZN, SJ, PS), pp. 43–54.
SACSAC-2011-ChangH #approach #model transformation #multi #using #verification
A model transformation approach for verifying multi-agent systems using SPIN (LC, XH), pp. 37–42.
SACSAC-2011-MammarFD #approach #reachability #verification
A proof-based approach to verifying reachability properties (AM, MF, FD), pp. 1651–1657.
ICSEICSE-2011-CassouBCL #architecture #development #verification
Leveraging software architectures to guide and verify the development of sense/compute/control applications (DC, EB, CC, JLL), pp. 431–440.
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.
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.
CGOCGO-2011-Leroy #compilation #how #question #verification #why
Formally verifying a compiler: Why? How? How far? (XL).
CAVCAV-2011-GuptaPR #concurrent #constraints #multi #named #source code #thread #verification
Threader: A Constraint-Based Verifier for Multi-threaded Programs (AG, CP, AR), pp. 412–417.
CAVCAV-2011-JhalaMR #functional #named #source code #using #verification
HMC: Verifying Functional Programs Using Abstract Interpreters (RJ, RM, AR), pp. 470–485.
LICSLICS-2011-GollerL #complexity #term rewriting #verification
The Complexity of Verifying Ground Tree Rewrite Systems (SG, AWL), pp. 279–288.
ICSTSAT-2011-DantsinH #satisfiability
Satisfiability Certificates Verifiable in Subexponential Time (ED, EAH), pp. 19–32.
VMCAIVMCAI-2011-GotmanovCK #communication #verification
Verifying Deadlock-Freedom of Communication Fabrics (AG, SC, MK), pp. 214–231.
DACDAC-2010-Coudert #algorithm #performance #verification
An efficient algorithm to verify generalized false paths (OC), pp. 188–193.
DATEDATE-2010-SoekenWKGD #modelling #ocl #satisfiability #uml #using #verification
Verifying UML/OCL models using Boolean satisfiability (MS, RW, MK, MG, RD), pp. 1341–1344.
ESOPESOP-2010-KoprowskiB #interpreter #named #parsing
TRX: A Formally Verified Parser Interpreter (AK, HB), pp. 345–365.
ESOPESOP-2010-Lochbihler #compilation #java #thread #verification
Verifying a Compiler for Java Threads (AL), pp. 427–447.
FASEFASE-2010-KimLK #approach #configuration management #data access #modelling
A Verifiable Modeling Approach to Configurable Role-Based Access Control (DKK, LL, SK), pp. 188–202.
ICSMEICSM-2010-KellensNDJP #cobol #design #outsourcing #verification
Verifying the design of an outsourced COBOL system with IntensiVE (AK, CN, TD, LJ, BVP), pp. 1–8.
PLDIPLDI-2010-TatlockL #compilation
Bringing extensibility to verified compilers (ZT, SL), pp. 111–121.
SASSAS-2010-HofmannKS #coq #verification
Verifying a Local Generic Solver in Coq (MH, AK, HS), pp. 340–355.
LATALATA-2010-SaeedloeiG #induction #realtime #verification
Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R) (NS, GG), pp. 536–548.
IFMIFM-2010-DaumSS #correctness
From Operating-System Correctness to Pervasively Verified Applications (MD, NS, MS), pp. 105–120.
ICFPICFP-2010-ArnoldHKBS #matrix #specification #verification
Specifying and verifying sparse matrix codes (GA, JH, ASK, RB, MS), pp. 249–260.
KEODKEOD-2010-AnjumHY #ontology #verification
Cross Domain Knowledge Verification — Verifying Knowledge in Foundation Ontology based Domain Ontologies (NAA, JAH, BY), pp. 339–342.
MODELSMoDELS-v1-2010-RahimW #code generation #consistency #semantics #state machine #verification
Verifying Semantic Conformance of State Machine-to-Java Code Generators (LAR, JW), pp. 166–180.
ECOOPECOOP-2010-StadenCM #execution #logic #object-oriented #specification #verification
Verifying Executable Object-Oriented Specifications with Separation Logic (SvS, CC, BM), pp. 151–174.
ECOOPECOOP-2010-SvendsenBP #verification
Verifying Generics and Delegates (KS, LB, MJP), pp. 175–199.
LOPSTRLOPSTR-2010-FioravantiPPS #evaluation #infinity #verification
Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation (FF, AP, MP, VS), pp. 164–183.
POPLPOPL-2010-Chlipala #compilation #functional
A verified compiler for an impure functional language (AC), pp. 93–106.
POPLPOPL-2010-MalechaMSW #database #relational #towards
Toward a verified relational database management system (JGM, GM, AS, RW), pp. 237–248.
POPLPOPL-2010-Myreen #compilation
Verified just-in-time compiler on x86 (MOM), pp. 107–118.
POPLPOPL-2010-TristanL #pipes and filters #validation
A simple, verified validator for software pipelining (JBT, XL), pp. 83–92.
ASPLOSASPLOS-2010-RomanescuLS #consistency #memory management #specification #verification
Specifying and dynamically verifying address translation-aware memory consistency (BFR, ARL, DJS), pp. 323–334.
CCCC-2010-BurckhardtMS #memory management #modelling #verification
Verifying Local Transformations on Relaxed Memory Models (SB, MM, VS), pp. 104–123.
HPDCHPDC-2010-GehaniK #multi #named #trust #verification
Mendel: efficiently verifying the lineage of data modified in multiple trust domains (AG, MK), pp. 227–239.
PPoPPPPoPP-2010-LiGKQ #source code #verification
A symbolic verifier for CUDA programs (GL, GG, RMK, DQ), pp. 357–358.
CAVCAV-2010-BallBLKL #framework #research #verification
The Static Driver Verifier Research Platform (TB, EB, VL, RK, JL), pp. 119–122.
CAVCAV-2010-CohenNS10a #composition #ltl #named #verification
SPLIT: A Compositional LTL Verifier (AC, KSN, YS), pp. 558–561.
CAVCAV-2010-ConwayB #data type #implementation #low level #verification
Verifying Low-Level Implementations of High-Level Datatypes (CLC, CB), pp. 306–320.
CAVCAV-2010-RepsLTBL #verification
There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code (TWR, JL, AVT, GB, AL), pp. 41–56.
ICSTICST-2010-BruckerBKW #generative #policy #testing
Verified Firewall Policy Transformations for Test Case Generation (ADB, LB, PK, BW), pp. 345–354.
IJCARIJCAR-2010-ChaudhuriDLM #proving #safety #verification
Verifying Safety Properties with the TLA+ Proof System (KC, DD, LL, SM), pp. 142–148.
VMCAIVMCAI-2010-Leino #concurrent #source code #verification
Verifying Concurrent Programs with Chalice (KRML), p. 2.
WICSA-ECSAWICSA-ECSA-2009-BritoRL #architecture #fault tolerance #verification
Verifying architectural variabilities in software fault tolerance techniques (PHSB, CMFR, RdL), pp. 231–240.
ESOPESOP-2009-BarthwalN #execution #parsing
Verified, Executable Parsing (AB, MN), pp. 160–174.
ESOPESOP-2009-LeinoM #concurrent #multi #source code #thread #verification
A Basis for Verifying Multi-threaded Programs (KRML, PM), pp. 378–393.
ESOPESOP-2009-SchaferEM #attribute grammar #coq #formal method #verification
Formalising and Verifying Reference Attribute Grammars in Coq (MS, TE, OdM), pp. 143–159.
TACASTACAS-2009-EmmiJKM #implementation #verification
Verifying Reference Counting Implementations (ME, RJ, EK, RM), pp. 352–367.
CSMRCSMR-2009-KellensSDJP #cobol #design #framework #named #verification
Cognac: A Framework for Documenting and Verifying the Design of Cobol Systems (AK, KDS, TD, LJ, BVP), pp. 199–208.
PLDIPLDI-2009-SchwerdfegerW #composition
Verifiable composition of deterministic grammars (AS, EVW), pp. 199–210.
PLDIPLDI-2009-TristanL #lazy evaluation #validation
Verified validation of lazy code motion (JBT, XL), pp. 316–326.
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.
CIAACIAA-2009-AtigT #communication #parallel #source code #verification
Verifying Parallel Programs with Dynamic Communication Structures (MFA, TT), pp. 145–154.
LATALATA-2009-JiraskovaP #automaton #self #verification
Converting Self-verifying Automata into Deterministic Automata (GJ, GP), pp. 458–468.
FMFM-2009-HarrisKCJR #bound #data flow #process #verification
Verifying Information Flow Control over Unbounded Processes (WRH, NK, SC, SJ, TWR), pp. 773–789.
FMFM-2009-LarsenLNP #realtime #requirements #verification
Verifying Real-Time Systems against Scenario-Based Requirements (KGL, SL, BN, SP), pp. 676–691.
FMFM-2009-LeinenbachS #verification
Verifying the Microsoft Hyper-V Hypervisor with VCC (DL, TS), pp. 806–809.
FMFM-2009-OHalloran #verification
Guess and Verify — Back to the Future (CO), pp. 23–32.
IFMIFM-2009-CabotCR #contract #ocl #uml #verification
Verifying UML/OCL Operation Contracts (JC, RC, DR), pp. 40–55.
SEFMSEFM-2009-EzekielL #approach #automation #multi #verification
An Automated Approach to Verifying Diagnosability in Multi-agent Systems (JE, AL), pp. 51–60.
ICFPICFP-2009-KleinDE #case study #experience #kernel #verification
Experience report: seL4: formally verifying a high-performance microkernel (GK, PD, KE), pp. 91–96.
HCIHCI-AUII-2009-DetweilerB #guidelines #online #towards #trust
Trust in Online Technology: Towards Practical Guidelines Based on Experimentally Verified Theory (CD, JB), pp. 605–614.
CAiSECAiSE-2009-PlanasCG #action semantics #behaviour #modelling #semantics #specification #uml #verification
Verifying Action Semantics Specifications in UML Behavioral Models (EP, JC, CG), pp. 125–140.
SEKESEKE-2009-SloanKV
An Extendible Translation of BPEL to a Machine-verifiable Model (JCS, TMK, AV), pp. 344–349.
POPLPOPL-2009-GantyMR #liveness #source code #verification
Verifying liveness for asynchronous programs (PG, RM, AR), pp. 102–113.
POPLPOPL-2009-Ridge #approach #distributed #verification
Verifying distributed systems: the operational approach (TR), pp. 429–440.
SACSAC-2009-BiagioniDPS #distributed
Practical distributed voter-verifiable secret ballot system (EB, YD, WP, KS), pp. 16–21.
SLESLE-2009-SchwerdfegerW #composition #parsing
Verifiable Parse Table Composition for Deterministic Parsing (AS, EVW), pp. 184–203.
SPLCSPLC-2009-GanesanLAMB #architecture #design #product line #verification
Verifying architectural design rules of the flight software product line (DG, ML, CA, DM, MB), pp. 161–170.
LICSLICS-2009-GollerMT #complexity #on the #process #verification
On the Computational Complexity of Verifying One-Counter Processes (SG, RM, AWT), pp. 235–244.
VMCAIVMCAI-2009-Vafeiadis #abstraction #verification
Shape-Value Abstraction for Verifying Linearizability (VV), pp. 335–348.
DACDAC-2008-HoTDDGS #identification #logic #verification
Early formal verification of conditional coverage points to identify intrinsically hard-to-verify logic (RCH, MT, MMD, ROD, JG, DES), pp. 268–271.
DACDAC-2008-KuehlmannBCRMN #verification
Verifying really complex systems: on earth and beyond (AK, AB, DEC, RAR, RMM, AN), pp. 552–553.
DATEDATE-2008-KimSTDV #adaptation #constraints #online #refinement
Constraint Refinement for Online Verifiable Cross-Layer System Adaptation (MK, MOS, CLT, ND, NV), pp. 646–651.
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.
FASEFASE-2008-SmansJPS #automation #java #source code #verification
An Automatic Verifier for Java-Like Programs Based on Dynamic Frames (JS, BJ, FP, WS), pp. 261–275.
TACASTACAS-2008-FismanKL #distributed #fault tolerance #on the #protocol #verification
On Verifying Fault Tolerance of Distributed Protocols (DF, OK, YL), pp. 315–331.
ICALPICALP-C-2008-HallgrenKSZ #protocol #quantum #verification
Making Classical Honest Verifier Zero Knowledge Protocols Secure against Quantum Attacks (SH, AK, PS, SZ), pp. 592–603.
FMFM-2008-GrandyBSSR #protocol #security #verification
Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code (HG, MB, KS, GS, WR), pp. 165–180.
FMFM-2008-NollR #pointer #thread #verification
Verifying Dynamic Pointer-Manipulating Threads (TN, SR), pp. 84–99.
GT-VMTGT-VMT-2006-NarayananK08 #model transformation #towards #verification
Towards Verifying Model Transformations (AN, GK), pp. 191–200.
GT-VMTGT-VMT-2008-BaresiGMM #abstraction #graph transformation #using #verification
Using Graph Transformation Systems to Specify and Verify Data Abstractions (LB, CG, AM, MM).
GT-VMTGT-VMT-2008-NarayananK #model transformation #verification
Verifying Model Transformations by Structural Correspondence (AN, GK).
SEKESEKE-2008-PengDZ #behaviour #correctness #design pattern #implementation #verification
Verifying Behavioral Correctness of Design Pattern Implementation (TP, JD, YZ), pp. 454–459.
MODELSMoDELS-2008-ZamaniKB #enterprise #pattern matching #verification
A Pattern Language Verifier for Web-Based Enterprise Applications (BZ, SK, GB), pp. 553–567.
MODELSMoDELS-2008-ZamaniKB #enterprise #pattern matching #verification
A Pattern Language Verifier for Web-Based Enterprise Applications (BZ, SK, GB), pp. 553–567.
OOPSLAOOPSLA-2008-BeckmanBA #type system #verification
Verifying correct usage of atomic blocks and typestate (NEB, KB, JA), pp. 227–244.
GPCEGPCE-2008-DenneyF #automation #generative #verification
Generating customized verifiers for automatically generated code (ED, BF), pp. 77–88.
SACSAC-2008-XuWQ #modelling #using #verification
Modeling and verifying BPEL using synchronized net (CX, HW, WQ), pp. 2358–2362.
SACSAC-2008-ZuqueteA
Verifiable anonymous vote submission (AZ, FA), pp. 2159–2166.
SPLCSPLC-2008-Lutz #consistency #product line
Enabling Verifiable Conformance for Product Lines (RRL), pp. 35–44.
ICSTICST-2008-RamirezC #adaptation #logic #modelling #uml #verification
Verifying and Analyzing Adaptive Logic through UML State Models (AJR, BHCC), pp. 529–532.
ISSTAISSTA-2008-LoginovYCFRN #analysis #safety #verification
Verifying dereference safety via expanding-scope analysis (AL, EY, SC, SF, NR, MGN), pp. 213–224.
MBTMBT-2008-BruckerBW #empirical #proving #verification
Verifying Test-Hypotheses: An Experiment in Test and Proof (ADB, LB, BW), pp. 15–27.
ASEASE-2007-BlancGK #abstraction #c++ #verification
Verifying C++ with STL containers via predicate abstraction (NB, AG, DK), pp. 521–524.
ASEASE-2007-Leino #specification #verification
Specifying and verifying software (KRML), p. 2.
ESOPESOP-2007-BarthePR #bytecode #java #lightweight #verification
A Certified Lightweight Non-interference Java Bytecode Verifier (GB, DP, TR), pp. 125–140.
ESOPESOP-2007-LeinoS #invariant #using #verification
Using History Invariants to Verify Observers (KRML, WS), pp. 80–94.
TACASTACAS-2007-Leino #challenge #object-oriented #verification
Verifying Object-Oriented Software: Lessons and Challenges (KRML), p. 2.
CSMRCSMR-2007-SzegediGBGT #concept #java #slicing #source code #verification
Verifying the Concept of Union Slices on Java Programs (AS, TG, ÁB, TG, GT), pp. 233–242.
STOCSTOC-2007-GoldwasserGHKR #constant #verification
Verifying and decoding in constant depth (SG, DG, AH, TK, GNR), pp. 440–449.
IFMIFM-2007-AguirreRM #community #design #verification
Verifying Temporal Properties of CommUnity Designs (NA, GR, TSEM), pp. 1–20.
IFMIFM-2007-FaberJS #data type #parametricity #specification #verification
Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters (JF, SJ, VSS), pp. 233–252.
IFMIFM-2007-HanebergGRS #approach #smarttech #verification
Verifying Smart Card Applications: An ASM Approach (DH, HG, WR, GS), pp. 313–332.
SEFMSEFM-2007-GrandyBSR #encoding #named #protocol #security
ASN1-light: A Verified Message Encoding for Security Protocols (HG, RB, KS, WR), pp. 195–204.
SEFMSEFM-2007-SalehD #approach #novel #security #verification
Verifying Security Properties of Cryptoprotocols: A Novel Approach (MS, MD), pp. 349–360.
SEFMSEFM-2007-SchmittT #case study #verification
Verifying the Mondex Case Study (PHS, IT), pp. 47–58.
AGTIVEAGTIVE-2007-AnandK #assembly #generative #graph transformation
Code Graph Transformations for Verifiable Generation of SIMD-Parallel Assembly Code (CKA, WK), pp. 217–232.
AdaSIGAda-2007-LauW #component
Verified component-based software in SPARK: experimental results for a missile guidance system (KKL, ZW), pp. 51–58.
ICEISICEIS-EIS-2007-SomeN #case study #consistency #requirements #verification
Use Case Based Requirements Verification — Verifying the Consistency between Use Cases and Assertions (SSS, DKN), pp. 190–195.
PPDPPPDP-2007-BentonZ #compilation #formal method #semantics #verification
Formalizing and verifying semantic type soundness of a simple compiler (NB, UZ), pp. 1–12.
ICSEICSE-2007-Chalin #compilation #evolution #semantics #verification
A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler (PC), pp. 23–33.
CAVCAV-2007-AmitRRSY #abstraction #comparison #verification
Comparison Under Abstraction for Verifying Linearizability (DA, NR, TWR, MS, EY), pp. 477–490.
ICSTSAT-2007-Gelder #satisfiability #verification
Verifying Propositional Unsatisfiability: Pitfalls to Avoid (AVG), pp. 328–333.
TAPTAP-2007-BackEM #invariant #source code #testing #verification
Testing and Verifying Invariant Based Programs in the SOCOS Environment (RJB, JE, MM), pp. 61–78.
VMCAIVMCAI-2007-EmmiM #transaction #verification
Verifying Compensating Transactions (ME, RM), pp. 29–43.
ASEASE-2006-Futatsugi #proving #specification #verification
Verifying Specifications with Proof Scores in CafeOBJ (KF), pp. 3–10.
DATEDATE-2006-FrehseKR #abstraction #refinement #using #verification
Verifying analog oscillator circuits using forward/backward abstraction refinement (GF, BHK, RAR), pp. 257–262.
FASEFASE-2006-GiorgettiG #generative #ml #named #verification
JAG: JML Annotation Generation for Verifying Temporal Properties (AG, JG), pp. 373–376.
TACASTACAS-2006-ChakiCKRT #c #concurrent #message passing #recursion #source code #verification
Verifying Concurrent Message-Passing C Programs with Recursive Calls (SC, EMC, NK, TWR, TT), pp. 334–349.
ICALPICALP-v2-2006-Vergnaud #verification
New Extensions of Pairing-Based Signatures into Universal Designated Verifier Signatures (DV), pp. 58–69.
FMFM-2006-Woodcock #challenge
Verified Software Grand Challenge (JW), p. 617.
ICFPICFP-2006-Chlipala #composition #development #proving #verification
Modular development of certified program verifiers with a proof assistant (AC), pp. 160–171.
SOFTVISSOFTVIS-2006-JainCHB #evaluation #java
Experimental evaluation of animated-verifying object viewers for Java (JJ, JHCI, TDH, LAB), pp. 27–36.
SEKESEKE-2006-LeeDSG #approach #modelling #verification
A PVS Approach to Verifying ORA-SS Data Models (SUJL, GD, JS, LG), pp. 126–131.
SEKESEKE-2006-LeeK #architecture #case study #framework #re-engineering #verification
Verifying a Software Architecture Reconstruction Framework with a Case Study (SL, SK), pp. 102–107.
MODELSMoDELS-2006-PonsG #ocl #specification #verification
An OCL-Based Technique for Specifying and Verifying Refinement-Oriented Transformations in MDE (CP, DG), pp. 646–660.
MODELSMoDELS-2006-PonsG #ocl #specification #verification
An OCL-Based Technique for Specifying and Verifying Refinement-Oriented Transformations in MDE (CP, DG), pp. 646–660.
GPCEGPCE-2006-BradyH #compilation #interpreter #staged
A verified staged interpreter is a verified compiler (EB, KH), pp. 111–120.
GPCEGPCE-2006-CzarneckiP #constraints #ocl #verification
Verifying feature-based model templates against well-formedness OCL constraints (KC, KP), pp. 211–220.
LOPSTRLOPSTR-2006-MantelSK #data flow #proving #security #verification
Combining Different Proof Techniques for Verifying Information Flow Security (HM, HS, TK), pp. 94–110.
POPLPOPL-2006-LahiriQ #verification
Verifying properties of well-founded linked lists (SKL, SQ), pp. 115–126.
POPLPOPL-2006-MenonGMMSAP #compilation #optimisation #representation
A verifiable SSA program representation for aggressive compiler optimization (VM, NG, BRM, AM, TS, ARAT, LP), pp. 397–408.
HPCAHPCA-2006-ManovitH #consistency #memory management #verification
Completely verifying memory consistency of test program executions (CM, SH), pp. 166–175.
CAVCAV-2006-Hoare
The Ideal of Verified Software (CARH), pp. 5–16.
CAVCAV-2006-KrcalY #automaton #communication #verification
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify (PK, WY), pp. 249–262.
CSLCSL-2006-Ong #approach #infinity #semantics #verification
Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract) (CHLO), pp. 31–40.
IJCARIJCAR-2006-Chaieb #quantifier #verification
Verifying Mixed Real-Integer Quantifier Elimination (AC), pp. 528–540.
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.
ASEASE-2005-Grov #algorithm #approach #correctness #deduction #reasoning #source code #verification
Verifying the correctness of hume programs: an approach combining deductive and algorithmic reasoning (GG), pp. 444–447.
ASEASE-2005-VardhanV #branch #learning #verification
Learning to verify branching time properties (AV, MV), pp. 325–328.
ASEASE-2005-XuN #approach #modelling #verification
A threat-driven approach to modeling and verifying secure software (DX, KEN), pp. 342–346.
DACDAC-2005-JainKSC #abstraction #refinement #verification #word
Word level predicate abstraction and refinement for verifying RTL verilog (HJ, DK, NS, EMC), pp. 445–450.
SIGMODSIGMOD-2005-DeutschMSVZ #data-driven #interactive #verification #web
A Verifier for Interactive, Data-Driven Web Applications (AD, MM, LS, VV, DZ), pp. 539–550.
SIGMODSIGMOD-2005-PangJRT #query #relational #verification
Verifying Completeness of Relational Query Results in Data Publishing (HP, AJ, KR, KLT), pp. 407–418.
FASEFASE-2005-Berry #design #industrial #performance #specification
Esterel v7: From Verified Formal Specification to Efficient Industrial Designs (GB), p. 1.
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-VardhanSVA #using #verification
Using Language Inference to Verify ω-Regular Properties (AV, KS, MV, GA), pp. 45–60.
MSRMSR-2005-HuangL #learning #mining #process #verification #version control
Mining version histories to verify the learning process of Legitimate Peripheral Participants (SKH, KmL), pp. 21–25.
PLDIPLDI-2005-ElmasTQ #concurrent #detection #named #runtime #source code #verification
VYRD: verifYing concurrent programs by runtime refinement-violation detection (TE, ST, SQ), pp. 27–37.
ICALPICALP-2005-LipmaaWB #security #verification
Designated Verifier Signature Schemes: Attacks, New Security Notions and a New Construction (HL, GW, FB), pp. 459–471.
FMFM-2005-KatzK #specification #verification
Verifying Scenario-Based Aspect Specifications (EK, SK), pp. 432–447.
FMFM-2005-SalverdaRZ #parallel #verification
Formally Defining and Verifying Master/Slave Speculative Parallelization (PS, GR, CBZ), pp. 123–138.
AdaSIGAda-2005-NaeserLA #verification
Temporal skeletons for verifying time (GN, KL, LA), pp. 49–56.
SEKESEKE-2005-WangWH #hybrid #linear #verification
Verifying Timed and Linear Hybrid Rule-Systems with RED (FW, RSW, GDH), pp. 448–454.
PPDPPPDP-2005-CortierRZ #encryption #protocol #verification
A resolution strategy for verifying cryptographic protocols with CBC encryption and blind signatures (VC, MR, EZ), pp. 12–22.
ICSEICSE-2005-ChinKQPN #alias #policy #safety #verification
Verifying safety policies with size properties and alias controls (WNC, SCK, SQ, CP, HHN), pp. 186–195.
CCCC-2005-LamKR #consistency #data type #named #verification
Hob: A Tool for Verifying Data Structure Consistency (PL, VK, MCR), pp. 237–241.
PPoPPPPoPP-2005-YangBHM #correctness #monitoring #source code #trust #verification
Trust but verify: monitoring remotely executing programs for progress and correctness (SY, ARB, YCH, SPM), pp. 196–205.
SOSPSOSP-2005-SeshadriLSPDK #execution #legacy #named #verification
Pioneer: verifying code integrity and enforcing untampered code execution on legacy systems (AS, ML, ES, AP, LvD, PKK), pp. 1–16.
CAVCAV-2005-BalabanFPZ #invariant #named #verification
IIV: An Invisible Invariant Verifier (IB, YF, AP, LDZ), pp. 408–412.
CAVCAV-2005-ChanderEILN #java #named #verification
JVer: A Java Verifier (AC, DE, NI, PL, GCN), pp. 144–147.
CAVCAV-2005-Yavuz-KahveciBB #verification
Action Language Verifier, Extended (TYK, CB, TB), pp. 413–417.
LICSLICS-2005-AbdullaHM #finite #infinity #markov #verification
Verifying Infinite Markov Chains with a Finite Attractor or the Global Coarseness Property (PAA, NBH, RM), pp. 127–136.
VMCAIVMCAI-2005-AttieC #concurrent #scalability #source code
Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs (PCA, HC), pp. 465–481.
VMCAIVMCAI-2005-BurckhardtAM #composition #implementation #parametricity #refinement #safety #verification
Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement (SB, RA, MMKM), pp. 130–145.
VMCAIVMCAI-2005-Hoare #challenge #compilation #research #verification
The Verifying Compiler, a Grand Challenge for Computing Research (CARH), p. 78.
ASEASE-2004-Betin-CanB #concurrent #programming #using
Verifiable Concurrent Programming Using Concurrency Controllers (ABC, TB), pp. 248–257.
ASEASE-2004-LicataK #interactive #source code #verification #web
Verifying Interactive Web Programs (DRL, SK), pp. 164–173.
DACDAC-2004-LuJ #using #verification
Verifying a gigabit ethernet switch using SMV (YL, MJ), pp. 230–233.
DACDAC-2004-ShehataA #composition #verification
A general decomposition strategy for verifying register renaming (HIS, MA), pp. 234–237.
FoSSaCSFoSSaCS-2004-GenestMMP #partial order #specification #using #verification
Specifying and Verifying Partial Order Properties Using Template MSCs (BG, MM, AM, DP), pp. 195–210.
PLDIPLDI-2004-YahavR #abstraction #safety #using #verification
Verifying safety properties using separation and heterogeneous abstractions (EY, GR), pp. 25–34.
STOCSTOC-2004-HolmerinK #equation #linear #verification
A new PCP outer verifier with applications to homogeneous linear equations and max-bisection (JH, SK), pp. 11–20.
IFMIFM-2004-BallCLR #formal method #verification
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft (TB, BC, VL, SKR), pp. 1–20.
IFMIFM-2004-SchneiderT #component #verification
Verifying Controlled Components (SS, HT), pp. 87–107.
SEFMSEFM-2004-EvansTLF #how #information management #verification
How to Verify Dynamic Properties of Information Systems (NE, HT, RL, MF), pp. 416–425.
SIGIRSIGIR-2004-TsengT #categorisation #verification
Verifying a Chinese collection for text categorization (YHT, WJT), pp. 556–557.
ECOOPECOOP-2004-BeersSF #analysis
Efficiently Verifiable Escape Analysis (MQB, CHS, MF), pp. 75–95.
FSEFSE-2004-KrishnamurthiFG #verification
Verifying aspect advice modularly (SK, KF, MG), pp. 137–146.
ICSEICSE-2004-DongLLW #verification
Verifying DAML+OIL and Beyond in Z/EVES (JSD, CHL, YFL, HHW), pp. 201–210.
ICSEICSE-2004-Mariani #behaviour #component #evolution #verification
Behavior Capture and Test for Verifying Evolving Component-Based Systems (LM), pp. 78–80.
LDTALDTA-2004-GoldreiS #attribute grammar #formal method #off the shelf #using #verification
Using Off-the-Shelf Formal Methods to Verify Attribute Grammar Properties (SG, AMS), pp. 33–54.
CAVCAV-2004-BustanRV #markov #verification
Verifying ω-Regular Properties of Markov Chains (DB, SR, MYV), pp. 189–201.
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.
ICDARICDAR-2003-MuramatsuM #online #verification
An HMM On-line Signature Verifier Incorporating Signature Trajectories (DM, TM), pp. 438–442.
ESOPESOP-2003-YahavRSW #evolution #logic #verification
Verifying Temporal Heap Properties Specified via Evolution Logic (EY, TWR, SS, RW), pp. 204–222.
TACASTACAS-2003-BozgaLP #abstraction #protocol #verification
Pattern-Based Abstraction for Verifying Secrecy in Protocols (LB, YL, MP), pp. 299–314.
TACASTACAS-2003-DembinskiJJPPSWZ #automaton #named #specification #verification
Verics: A Tool for Verifying Timed Automata and Estelle Specifications (PD, AJ, PJ, WP, AP, MS, BW, AZ), pp. 278–283.
FMFME-2003-Fidge #legacy #verification
Verifying Emulation of Legacy Mission Computer Systems (CJF), pp. 187–207.
SEFMSEFM-2003-DeharbeR #debugging #proving #theorem proving #verification
Light-Weight Theorem Proving for Debugging and Verifying Units of Code (DD, SR), pp. 220–228.
AdaSIGAda-2003-EvangelistaKPR #ada #concurrent #linear #logic #source code #verification
Verifying linear time temporal logic properties of concurrent Ada programs with quasar (SE, CK, JFPP, PR), pp. 17–24.
SEKESEKE-2003-SongPLGCM #e-commerce #uml #verification
Extending UML to Specify and Verify E-commerce Systems (MAJS, AMP, FL, GG, SVAC, WMJ), pp. 306–313.
ESEC-FSEESEC-FSE-2003-JeffordsH #requirements #verification
A strategy for efficiently verifying requirements (RDJ, CLH), pp. 28–37.
ESEC-FSEESEC-FSE-2003-XieB #component #composition
Verified systems by composition from verified components (FX, JCB), pp. 277–286.
LDTALDTA-2003-Lee #framework
A Formally Verified Register Allocation Framework (KL), pp. 515–531.
CCCC-2003-Hoare #challenge #compilation #research #verification
The Verifying Compiler: A Grand Challenge for Computing Research (CARH), pp. 262–272.
VMCAIVMCAI-2003-BossiFPR #bisimulation #security #verification
Bisimulation and Unwinding for Verifying Possibilistic Security Properties (AB, RF, CP, SR), pp. 223–237.
VMCAIVMCAI-2003-WinEGKL #algorithm #distributed #execution #using #verification
Using Simulated Execution in Verifying Distributed Algorithms (TNW, MDE, SJG, DKK, NAL), pp. 283–297.
CBSECBSE-2003-DijkmanAQ #component #correctness #process #verification
Verifying the Correctness of Component-Based Applications that Support Business Processes (RMD, JAA, DAQ), p. 8.
DACDAC-2002-SemeriaMPESN #concurrent #design #multi #thread #verification
RTL c-based methodology for designing and verifying a multi-threaded processor (LS, RM, BMP, AE, AS, DN), pp. 123–128.
DATEDATE-2002-HassounCC #verification
Verifying Clock Schedules in the Presence of Cross Talk (SH, ECG, CC), pp. 346–350.
DATEDATE-2002-Velev #similarity #using #verification
Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer (MNV), pp. 28–35.
PODSPODS-2002-ArenasFL #consistency #on the #specification #verification #xml
On Verifying Consistency of XML Specifications (MA, WF, LL), pp. 259–270.
FoSSaCSFoSSaCS-2002-SchoppS #process #using #verification
Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes (US, AKS), pp. 372–386.
WCREWCRE-2002-TanT #fault #program analysis #transaction #verification
Verifying Provisions for Post-Transaction User Input Error Correction through Static Program Analysis (HBKT, NLT), p. 233–?.
STOCSTOC-2002-ColeH #verification
Verifying candidate matches in sparse and wildcard matching (RC, RH), pp. 592–601.
FMFME-2002-ArtsED #case study #erlang #verification
Verifying Erlang Code: A Resource Locker Case-Study (TA, CBE, JD), pp. 184–203.
FMFME-2002-BackesJP #bisimulation #composition #encryption #implementation #using
Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation (MB, CJ, BP), pp. 310–329.
FMFME-2002-Casset #development #embedded #formal method #java #using #verification
Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods (LC), pp. 290–309.
IFMIFM-2002-XiongCTB
Formally Linking MDG and HOL Based on a Verified MDG System (HX, PC, ST, AB), pp. 205–224.
SEKESEKE-2002-ArandaM #design pattern #formal method #verification
A formal model for verifying compound design patterns (GNA, RM), pp. 213–214.
SEKESEKE-2002-BarbutiTBF #bytecode #java #verification
Fixing the Java bytecode verifier by a suitable type domain (RB, LT, CB, NDF), pp. 377–382.
SEKESEKE-2002-XuVIY #behaviour #modelling #multi #using #verification
Modeling and verifying multi-agent behaviors using predicate/transition nets (DX, RAV, TRI, JY), pp. 193–200.
LOPSTRLOPSTR-2002-GutierrezR #calculus #type system #verification
A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene (FG, BCR), pp. 17–31.
FSEFSE-2002-LiKF #verification
Verifying cross-cutting features as open systems (HCL, SK, KF), pp. 89–98.
ICSEICSE-2002-AtiyaK #concurrent #verification
A compliance notation for verifying concurrent systems (DMA, SK), pp. 731–732.
CAVCAV-2002-BryantLS #logic #modelling #using #verification
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with λ Expressions and Uninterpreted Functions (REB, SKL, SAS), pp. 78–92.
ICTSSTestCom-2002-Veciana-NoguesCDS #metric #verification
Verifying IP Meters from Sampled Measurements (CVN, ACA, JDP, JSP), pp. 39–54.
VMCAIVMCAI-2002-KrsticM #algorithm #monad #verification
Verifying BDD Algorithms through Monadic Interpretation (SK, JM), pp. 182–195.
CBSECBSE-2001-FislerKB #collaboration #component #design #verification
Verifying Component-Based Collaboration Designs (KF, SK, DSB), p. 17.
ASEASE-2001-BultanY #verification
Action Language Verifier (TB, TYK), pp. 382–386.
ASEASE-2001-Xia #mobile #verification
Verify Properties of Mobile Code (SX), p. 440.
FASEFASE-2001-ReusWH #calculus #design #hoare #java #modelling #ocl #verification
A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models (BR, MW, RH), pp. 300–317.
FoSSaCSFoSSaCS-2001-Nipkow #bytecode #verification
Verified Bytecode Verifiers (TN), pp. 347–363.
STOCSTOC-2001-GennaroIKR #complexity #multi
The round complexity of verifiable secret sharing and secure multicast (RG, YI, EK, TR), pp. 580–589.
FMFME-2001-BurtonKP #implementation #verification
Verifying Implementation Relations (JB, MK, GP), pp. 364–383.
POPLPOPL-2001-Yahav #concurrent #java #logic #safety #source code #using #verification
Verifying safety properties of concurrent Java programs using 3-valued logic (EY), pp. 27–40.
SACSAC-2001-KallesK #design #game studies #learning #on the #using #verification
On verifying game designs and playing strategies using reinforcement learning (DK, PK), pp. 6–11.
FSEESEC-FSE-2001-Coen-PorisiniDGP #execution #safety #symbolic computation #using #verification
Using symbolic execution for verifying safety-critical systems (ACP, GD, CG, MP), pp. 142–151.
CAVCAV-2001-AlurW #implementation #network #protocol #refinement #verification
Verifying Network Protocol Implementations by Symbolic Refinement Checking (RA, BYW), pp. 169–181.
CAVCAV-2001-Arons #consistency #using #verification
Using Timestamping and History Variables to Verify Sequential Consistency (TA), pp. 423–435.
CAVCAV-2001-Bertot #formal method #proving #theorem proving #verification
Formalizing a JVML Verifier for Initialization in a Theorem Prover (YB), pp. 14–24.
RTARTA-2001-KorovinV #order #using #verification
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order (KK, AV), pp. 137–153.
CBSECBSE-2000-RíoGL #component #named #verification
Itacio: A Component Model for Verifying Software at Construction Time (ACdR, JELG, JMCL), p. 12.
FoSSaCSFoSSaCS-2000-BerardLS #equivalence #parallel #performance #process #verification
Verifying Performance Equivalence for Timed Basic Parallel Processes (BB, AL, PS), pp. 35–47.
TACASTACAS-2000-BaukusBLS #network #verification
Abstracting WS1S Systems to Verify Parameterized Networks (KB, SB, YL, KS), pp. 188–203.
TACASTACAS-2000-JonssonN #infinity #transitive #verification
Transitive Closures of Regular Relations for Verifying Infinite-State Systems (BJ, MN), pp. 220–234.
STOCSTOC-2000-CramerDD #complexity #multi #on the
On the complexity of verifiable secret sharing and multiparty computation (RC, ID, SD), pp. 325–334.
IFLIFL-2000-ArtsN #erlang #implementation #verification
Verifying Generic Erlang Client-Server Implementations (TA, TN), pp. 37–52.
POPLPOPL-2000-VolpanoS #verification
Verifying Secrets and Relative Secrecy (DMV, GS), pp. 268–276.
SACSAC-2000-DoyonD #bytecode #java #verification
Verifying Object Initialization in the Java Bytecode Language (SD, MD), pp. 821–830.
CAVCAV-2000-Cohen #encryption #first-order #named #protocol #verification
TAPS: A First-Order Verifier for Cryptographic Protocols (EC), pp. 568–571.
CAVCAV-2000-HosabettuGS #architecture #exception #verification
Verifying Advanced Microarchitectures that Support Speculation and Exceptions (RH, GG, MKS), pp. 521–537.
ISSTAISSTA-2000-CobleighCO #process #verification
Verifying properties of process definitions (JMC, LAC, LJO), pp. 96–101.
ASEASE-1999-LiliusP #modelling #named #uml #verification
vUML: A Tool for Verifying UML Models (JL, IP), pp. 255–258.
DACDAC-1999-AbtsR #multi #scalability #using #verification
Verifying Large-Scale Multiprocessors Using an Abstract Verification Environment (DA, MR), pp. 163–168.
DATEDATE-1999-HendricxC
Formally Verified Redundancy Removal (SH, LJMC), p. 150–?.
DATEDATE-1999-HuhnSKL #verification
Verifying Imprecisely Working Arithmetic Circuits (MH, KS, TK, GL), p. 65–?.
ICDARICDAR-1999-LeeL #automation #design #empirical #sorting #verification
Empirical Design of a Holistic Verifier for Automatic Sorting of Handwritten Singapore Postal Addresses (CKL, GL), pp. 733–736.
ITiCSEITiCSE-1999-Kosa #verification #web
Beginners program Web page builders and verifiers (MJK), p. 185.
TACASTACAS-1999-Pusch #bytecode #higher-order #java #proving #specification #verification
Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL (CP), pp. 89–103.
CIAAWIA-1999-Trahtman #algorithm #automaton #finite #testing #verification
An Algorithm to Verify Local Threshold Testability of Deterministic Finite Automata (ANT), pp. 164–173.
FMFM-v1-1999-ArtsD #database #distributed #erlang #verification
Verifying a Distributed Database Lookup Manager Written in Erlang (TA, MD), pp. 682–700.
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-Liu #consistency #specification #testing #verification
Verifying Consistency and Validity of Formal Specifications by Testing (SL), pp. 896–914.
FMFM-v2-1999-MoriF #behaviour #specification #verification
Verifying Behavioural Specifications in CafeOBJ Environment (AM, KF), pp. 1625–1643.
OOPSLAOOPSLA-1999-FreundM #bytecode #framework #java #verification
A Formal Framework for the Java Bytecode Language and Verifier (SNF, JCM), pp. 147–166.
ICSEICSE-1999-HolzmannS #verification
A Practical Method for Verifying Event-Driven Software (GJH, MHS), pp. 597–607.
CADECADE-1999-AdamsGLM #named
VSDITLU: a verifiable symbolic definite integral table look-up (AAA, HG, SL, UM), pp. 112–126.
CAVCAV-1999-CimattiCGR #named #verification
NUSMV: A New Symbolic Model Verifier (AC, EMC, FG, MR), pp. 495–499.
CAVCAV-1999-HenzingerQR99a #consistency #multi #verification
Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems (TAH, SQ, SKR), pp. 301–315.
CSLCSL-1999-KestenP #abstraction #liveness #verification
Verifying Liveness by Augmented Abstraction (YK, AP), pp. 141–156.
ASEASE-1998-OHalloranS #exclamation #verification
Don’t Verify, Abstract! (CO, AS), pp. 53–62.
ESOPESOP-1998-CairesM #concurrent #execution #logic #specification
Verifiable and Executable Logic Specifications of Concurrent Objects in Lpi (LC, LM), pp. 42–56.
TACASTACAS-1998-AbdullaJ #network #process #verification
Verifying Networks of Timed Processes (Extended Abstract) (PAA, BJ), pp. 298–312.
TACASTACAS-1998-Sprenger #calculus #coq #model checking #μ-calculus
A Verified Model Checker for the Modal μ-calculus in Coq (CS), pp. 167–183.
CSMRCSMR-1998-OhtaMI #on the #source code #verification
On Constructing a Tool to Verify Programs for Processors Built in Machines (TO, NM, YI), pp. 52–59.
STOCSTOC-1998-GoldreichSV #statistics
Honest-Verifier Statistical Zero-Knowledge Equals General Statistical Zero-Knowledge (OG, AS, SPV), pp. 399–408.
CAVCAV-1998-FerrariGMPR #mobile #process #verification
Verifying Mobile Processes in the HAL Environment (GLF, SG, UM, MP, GR), pp. 511–515.
CAVCAV-1998-SternD #in memory #memory management #using #verification
Using Magnatic Disk Instead of Main Memory in the Murphi Verifier (US, DLD), pp. 172–183.
CAVCAV-1998-WolperB #infinity #verification
Verifying Systems with Infinite but Regular State Spaces (PW, BB), pp. 88–97.
ISSTAISSTA-1998-BultanGL #approach #constraints #integer #verification
Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach (TB, RG, CL), pp. 113–123.
LICSLICS-1998-Alfaro #behaviour #how #probability #verification
How to Specify and Verify the Long-Run Average Behavior of Probabilistic Systems (LdA), pp. 454–465.
ASEASE-1997-FenselS #architecture #knowledge-based #using #verification
Using KIV to Specify and Verify Architectures of Knowledge-Based Systems (DF, AS), p. 71–?.
TACASTACAS-1997-Prasetya #algorithm #self
Mechanically Verified Self-Stabilizing Hierarchical Algorithms (ISWBP), pp. 399–415.
FMFME-1997-HemerL #design #pattern matching #reuse
Reuse of Verified Design Templates Through Extended Pattern Matching (DH, PAL), pp. 495–514.
AdaEuropeAdaEurope-1997-PierceAWSCG #performance #realtime #requirements #verification
Capturing and Verifying Performance Requirements for Hard Real Time Systems (RHP, SA, RW, JS, HC, JG), pp. 137–148.
AdaTRI-Ada-1997-RileyDP #analysis #implementation #verification
An Instance of the Application Download Pattern: The SPAIDS Software Loader/Verifier Domain Analysis and Implementation (JDR, SD, WP), pp. 273–278.
ICSEICSE-1997-HeitmeyerKL #requirements #specification #tool support #validation #verification
The SCR Method for Formally Specifying, Verifying, and Validating Requirements: Tool Support (CLH, JK, BGL), pp. 610–611.
CAVCAV-1997-Berry #design #verification
Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design (GB), p. 303.
CAVCAV-1997-CimattiGPPPRTY #certification #embedded #safety #verification
A Provably Correct Embedded Verifier for the Certification of Safety Critical Software (AC, FG, PP, BP, JP, DR, PT, BY), pp. 202–213.
CAVCAV-1997-PandeyB #evaluation #symmetry #verification
Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation (MP, REB), pp. 244–255.
CAVCAV-1997-SternD #verification
Parallelizing the Murphi Verifier (US, DLD), pp. 256–278.
DACDAC-1996-Burch #verification
Techniques for Verifying Superscalar Microprocessors (JRB), pp. 552–557.
DACDAC-1996-DesaiY #cpu #design #simulation #using #verification
A Systematic Technique for Verifying Critical Path Delays in a 300MHz Alpha CPU Design Using Circuit Simulation (MPD, YTY), pp. 125–130.
PODSPODS-1996-BenediktGL #database #transaction
Verifiable Properties of Database Transactions (MB, TG, LL), pp. 117–127.
TACASTACAS-1996-CleavelandLNS #distributed #modelling #verification
Priorities for Modeling and Verifying Distributed Systems (RC, GL, VN, SS), pp. 278–297.
SACSAC-1996-Gurr #logic programming #specification
Verifiable partial specifications for logic programming (CAG), pp. 374–379.
CAVCAV-1996-AzizSSB #markov #verification
Verifying Continuous Time Markov Chains (AA, KS, VS, RKB), pp. 269–276.
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-ClarkeGZ #algorithm #proving #theorem proving #using #verification
Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.
CAVCAV-1996-Gonthier #concurrent #garbage collection #safety #verification
Verifying the Safety of a Practical Concurrent Garbage Collector (GG), pp. 462–465.
CAVCAV-1996-GrafS #invariant #proving #theorem proving #using #verification
Verifying Invariants Using theorem Proving (SG, HS), pp. 196–207.
CAVCAV-1996-Greenstreet #difference #equation #safety #verification
Verifying Safety Properties of Differential Equations (MRG), pp. 277–287.
CAVCAV-1996-IpD #component #verification
Verifying Systems with Replicated Components in Murphi (CNI, DLD), pp. 147–158.
CAVCAV-1996-KapurS #multi #product line #verification
Mechanically Verifying a Family of Multiplier Circuits (DK, MS), pp. 135–146.
PPDPPLILP-1995-Fasbender #implementation
A Verified Implementation of Narrowing (HF), pp. 63–80.
PPDPPLILP-1995-Hatcliff #correctness #verification
Mechanically Verifying the Correctness of an Offline Partial Evaluator (JH), pp. 279–298.
POPLPOPL-1995-BouajjaniEH #composition #infinity #parallel #process #verification
Verifying Infinite State Processes with Sequential and Parallel Composition (AB, RE, PH), pp. 95–106.
ESECESEC-1995-TuyaSC #model checking #modelling #safety #using #verification
Using a Symbolic Model Checker for Verify Safety Properties in SA/RT Models (JT, LS, JAC), pp. 59–75.
CAVCAV-1995-BouajjaniR #hybrid #linear #subclass #verification
Verifying ω-Regular Properties for a Subclass of Linear Hybrid Systems (AB, RR), pp. 437–450.
CAVCAV-1995-FidgeKU #realtime #verification
Interactively Verifying a Simple Real-time Scheduler (CJF, PK, MU), pp. 395–408.
CAVCAV-1995-JonssonK #algorithm #distributed #infinity #safety #verification
Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms (BJ, LK), pp. 42–53.
TLCATLCA-1995-Pollack
A Verified Typechecker (RP), pp. 365–380.
DACDAC-1994-BeattyB #simulation #using #verification
Formally Verifying a Microprocessor Using a Simulation Methodology (DLB, REB), pp. 596–602.
DATEEDAC-1994-KeM #synthesis
Synthesis of Delay-Verifiable Two-Level Circuits (WK, PRM), pp. 297–301.
FMFME-1994-Evans #concurrent #specification #using #verification
Specifying & Verifying Concurrent Systems Using Z (AE), pp. 366–380.
FMFME-1994-StoreyH #using
A Strategy for the Production of Verifiable Code Using the B Method (AS, HPH), pp. 346–365.
FSEFSE-1994-DwyerC #analysis #concurrent #data flow #source code #verification
Data Flow Analysis for Verifying Properties of Concurrent Programs (MBD, LAC), pp. 62–75.
ICLPICLP-1994-Diel #towards
Towards a Verified OR-Parallel WAM (SD), pp. 737–738.
SEKESEKE-1993-KushnerE #experience #rule-based #verification
Experience Verifying a Rule-based Program as Part of a Cleanroom Project: AOEXPERT/MVS (TRK, DSE), pp. 445–452.
TOOLSTOOLS-USA-1993-GlykasWH #design #object-oriented
Verifiable Object Oriented Designs (MG, PW, TH), pp. 391–406.
CAVCAV-1993-Gordon #imperative #source code #verification
A Verifier and Timing Analyser for Simple Imperative Programs (Abstract) (MJCG), p. 320.
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-JourdanMO #realtime #source code #verification
Verifying Quantitative Real-Time Properties of Synchronous Programs (MJ, FM, AO), pp. 347–358.
CAVCAV-1993-KuttyRMDM #concurrent #logic #tool support #verification #visual notation
A Graphical Interval Logic Toolset for Verifying Concurrent Systems (GK, YSR, LEM, LKD, PMMS), pp. 138–153.
CAVCAV-1993-ProbstL #automaton #behaviour #verification
Verifying Timed Behavior Automata with Input/Output Critical Races (DKP, HFL), pp. 424–437.
CAVCAV-1993-Wilding
A Mechanically Verified Application for a Mechanically Verified Environment (MW), pp. 268–279.
ICALPICALP-1992-SantisPY #bound #proving #statistics #verification
One-Message Statistical Zero-Knowledge Proofs and Space-Bounded Verifier (ADS, GP, MY), pp. 28–40.
CADECADE-1992-Reif
The KIV System: Systematic Construction of Verified Software (WR), pp. 753–757.
CAVCAV-1992-AagaardL #case study #logic #synthesis #verification
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification (MA, ML), pp. 69–81.
CAVCAV-1992-Corbett #integer #liveness #programming #safety #verification
Verifying General Safety and Liveness Propterties with Integer Programming (JCC), pp. 357–369.
CAVCAV-1992-De-LeonG #abstraction #composition #distributed #realtime #verification
Modular Abstractions for Verifying Real-Time Distributed Systems (HDL, OG), pp. 2–15.
CAVCAV-1992-ProbstL #automaton #behaviour #constraints #verification
Verifying Timed Behavior Automata with Nonbinary Delay Constraints (DKP, HFL), pp. 123–136.
DACDAC-1991-Burch #multi #using #verification
Using BDDs to Verify Multipliers (JRB), pp. 408–412.
DACDAC-1991-BuschV #design #hardware
Proof-Aided Design of Verified Hardware (HB, GV), pp. 391–396.
PEPMPEPM-1991-McNerney #abstract interpretation #compilation #correctness #using #verification
Verifying the Correctness of Compiler Transformations on Basic Blocks using Abstract Interpretation (TSM), pp. 106–115.
CAVCAV-1991-GabrielianI #realtime #specification #verification
Verifying Properties of HMS Machine Specifications of Real-Time Systems (AG, RI), pp. 421–431.
CAVCAV-1991-Goldschlag #liveness #safety #verification
Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits (DMG), pp. 354–364.
CAVCAV-1991-NicolaFGR #behaviour #concurrent #framework #logic #verification
An Action Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems (RDN, AF, SG, GR), pp. 37–47.
PLDIPLDI-1990-Giegerich #code generation #on the #specification
On the Structure of Verifiable Code Generator Specifications (RG), pp. 1–8.
PPDPPLILP-1990-BowenJP #approach #compilation #prototype #specification
An Approach to Verifiable Compiling Specification and Prototyping (JPB, JH, PKP), pp. 45–59.
CADECADE-1990-KaflZ #proving #theorem proving #verification
The Theorem Prover of the Program Verifier Tatzelwurm (TK, NZ), pp. 657–658.
CAVCAV-1990-Burch #liveness #safety #verification
Verifying Liveness Properties by Verifying Safety Properties (JRB), pp. 224–232.
CAVCAV-1990-CoudertMB #diagrams #verification
Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams (OC, JCM, CB), pp. 23–32.
CAVCAV-1990-LaiPD #on the #protocol #using #verification
On Using Protean To Verify ISO FTAM Protocol (RL, KRP, TSD), pp. 126–135.
CAVCAV-1990-NakamuraKFT #logic #using #verification
A Data Path Verifier for Register Transfer Level Using Temporal Logic Language Tokio (HN, YK, MF, HT), pp. 76–85.
STOCSTOC-1989-Kenyon-MathieuK #partial order #verification
Verifying Partial Orders (CKM, VK), pp. 367–374.
STOCSTOC-1989-RabinB #multi #protocol
Verifiable Secret Sharing and Multiparty Protocols with Honest Majority (Extended Abstract) (TR, MBO), pp. 73–85.
LICSLICS-1989-Pfenning #logic #metaprogramming #named
Elf: A Language for Logic Definition and Verified Metaprogramming (FP), pp. 313–322.
ISSTATAV-1989-Young #compilation
Verified Compilation in micro-Gypsy (WDY), pp. 20–26.
DACDAC-1988-WallaceS #named #verification
ATV: An Abstract Timing Verifier (DEW, CHS), pp. 154–159.
ICSEICSE-1988-CraigenKMNPS #named #verification
m-EVES: A Tool for Verifying Software (DC, SK, IM, AN, BP, MS), pp. 324–333.
ICALPICALP-1987-LarsenM #bisimulation #protocol #using #verification
Verifying a Protocol Using Relativized Bisimulation (KGL, RM), pp. 126–135.
ESECESEC-1987-Conradi #documentation #experience #fault #fortran #source code #verification
Experience with Fortran Verifier. A Tool for Documentation and Error Diagnosis of Fortran-77 Programs (RC), pp. 263–275.
DACDAC-1986-GlesnerSS #compilation #named #statistics #verification
SCAT — a new statistical timing verifier in a silicon compiler system (MG, JS, RBS), pp. 220–226.
DACDAC-1986-OdawaraTOOZ #comparison #logic #verification
A logic verifier based on Boolean comparison (GO, MT, OO, TO, ZqZ), pp. 208–214.
DACDAC-1986-SupowitF #verification
A new method for verifying sequential circuits (KJS, SJF), pp. 200–207.
DACDAC-1986-WallaceS #modelling #plugin #verification
Plug-in timing models for an abstract timing verifier (DEW, CHS), pp. 683–689.
CADECADE-1986-Kafl #linear #reasoning #verification
Program Verifier “Tatzelwurm”: Reasoning about Systems of Linear Inequalities (TK), pp. 300–305.
POPLPOPL-1983-Nelson #invariant #reachability #verification
Verifying Reachability Invariants of Linked Structures (GN), pp. 38–47.
DACDAC-1982-TakashimaMCY #source code #verification
Programs for verifying circuit connectivity of mos/lsi mask artwork (MT, TM, TC, KY), pp. 544–550.
DACDAC-1980-KoppelmanM #logic #verification
Verifying deep logic hierarchies with ALEX (GMK, KM), pp. 328–335.
POPLPOPL-1980-Pratt #on the #specification #verification
On Specifying Verifiers (VRP), pp. 106–116.
DACDAC-1977-ThomasS #automation #design #performance #verification
Measuring designer performance to verify design automation systems (DET, DPS), pp. 411–418.
ICALPICALP-1976-Cartwright #data type #lisp #source code #verification
User-Defined Data Types as an Aid to Verifying LISP Programs (RC), pp. 228–256.
POPLPOPL-1976-GriffithsP #process #specification #verification
Verifying Formal Specifications of Synchronous Processes (PPG, CJP), pp. 192–208.
SOSPSOSP-J-1975-OwickiG76 #approach #axiom #parallel #source code #verification
Verifying Properties of Parallel Programs: An Axiomatic Approach (SSO, DG), pp. 279–285.

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.