Stem verifi$ (all stems)

556 papers:

CASE-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.

DAC-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.

DAC-2015-HerdtLD #simulation #using #verification

Verifying SystemC using stateful symbolic simulation (VH, HML, RD), p. 6.

DATE-2015-MadhukarSWKM #abstraction #lazy evaluation #using #verification

Verifying synchronous reactive systems using lazy abstraction (KM, MS, BW, DK, RM), pp. 1571–1574.

ESOP-2015-EberlHN #compilation #probability

A Verified Compiler for Probability Density Functions (ME, JH, TN), pp. 80–104.

ESOP-2015-SergeyNB #algorithm #concurrent #specification #verification

Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity (IS, AN, AB), pp. 333–358.

FASE-2015-CzechJW #exclamation #verification #what

Just Test What You Cannot Verify! (MC, MCJ, HW), pp. 100–114.

TACAS-2015-Beyer #verification

Software Verification and Verifiable Witnesses — (Report on SV-COMP 2015) (DB), pp. 401–416.

TACAS-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.

TACAS-2015-GurfinkelKN #c #contest #framework #named #source code #verification

SeaHorn: A Framework for Verifying C Programs (Competition Contribution) (AG, TK, JAN), pp. 447–450.

TACAS-2015-HaranCELQR #composition #contest #verification

SMACK+Corral: A Modular Verifier — (Competition Contribution) (AH, MC, ME, AL, SQ, ZR), pp. 451–454.

TACAS-2015-Immler #analysis #reachability

Verified Reachability Analysis of Continuous Systems (FI), pp. 37–51.

TACAS-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.

TACAS-2015-TomascoI0TP15a #concurrent #memory management #source code #verification

Verifying Concurrent Programs by Memory Unwinding (ET, OI, BF, SLT, GP), pp. 551–565.

PEPM-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.

PLDI-2015-GammieHE #garbage collection #on the fly

Relaxing safely: verified on-the-fly garbage collection for x86-TSO (PG, ALH, KE), pp. 99–109.

PLDI-2015-TassarottiDV #logic #memory management #verification

Verifying read-copy-update in a logic for weak memory (JT, DD, VV), pp. 110–120.

PLDI-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.

FM-2015-BratBDGHK #safety #verification

Verifying the Safety of a Flight-Critical System (GB, DHB, MD, DG, FH, TK), pp. 308–324.

FM-2015-DerrickDSTW #transaction #verification

Verifying Opacity of a Transactional Mutex Lock (JD, BD, GS, OT, HW), pp. 161–177.

FM-2015-LiSLD #protocol #security #verification

Verifying Parameterized Timed Security Protocols (LL, JS, YL, JSD), pp. 342–359.

FM-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.

FM-2015-PolikarpovaTF #library

A Fully Verified Container Library (NP, JT, CAF), pp. 414–434.

SEFM-2015-Muhlberg0DLP #learning #source code #verification

Learning Assertions to Verify Linked-List Programs (JTM, DHW, MD, GL, FP), pp. 37–52.

SEFM-2015-Vanspauwen0 #encryption #implementation #library #protocol #specification #verification

Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications (GV, BJ), pp. 53–68.

ICFP-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.

ICGT-2015-Stuckrath #analysis #graph transformation #named #using #verification

Uncover: Using Coverability Analysis for Verifying Graph Transformation Systems (JS), pp. 266–274.

SEKE-2015-LiuH #petri net #pipes and filters #verification

PIPE+Verifier — A Tool for Analyzing High Level Petri Nets (SL, XH), pp. 575–580.

MoDELS-2015-OakesTLW #atl #contract #declarative #verification

Fully verifying transformation contracts for declarative ATL (BJO, JT, LL, MW), pp. 256–265.

MoDELS-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.

ECOOP-2015-SchwerhoffS #automation #lightweight #verification

Lightweight Support for Magic Wands in an Automatic Verifier (MS, AJS), pp. 614–638.

ECOOP-2015-VekrisCJ #trust #type system #verification

Trust, but Verify: Two-Phase Typing for Dynamic Languages (PV, BC, RJ), pp. 52–75.

OOPSLA-2015-BastaniAA #android #data flow #verification

Interactively verifying absence of explicit information flows in Android apps (OB, SA, AA), pp. 299–315.

OOPSLA-2015-WickersonBBD

Remote-scope promotion: clarified, rectified, and verified (JW, MB, BMB, AFD), pp. 731–747.

POPL-2015-JourdanLBLP #c

A Formally-Verified C Static Analyzer (JHJ, VL, SB, XL, DP), pp. 247–259.

SAC-2015-CostaCFR #diagrams #modelling #precise #uml

From UML diagrams to simulink models: a precise and verified translation (AC, SAdCC, LF, LR), pp. 1547–1552.

SAC-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.

SAC-2015-LeTN #requirements #using #verification

Verifying eventuality properties of imprecise system requirements using event-B (HAL, NTT, SN), pp. 1651–1653.

ESEC-FSE-2015-0001DDHS #validation #verification

Witness validation and stepwise testification across software verifiers (DB, MD, DD, MH, AS), pp. 721–733.

ICSE-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.

CC-2015-DemangePS #coq #optimisation #performance #verification

Verifying Fast and Sparse SSA-Based Optimizations in Coq (DD, DP, LS), pp. 233–252.

LCTES-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.

CAV-2015-Leslie-HurdCF #verification

Verifying Linearizability of Intel® Software Guard Extensions (RLH, DC, MF), pp. 144–160.

ICST-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.

ICST-2015-ZhangAC #exclamation #model checking #verification

Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications (HZ, TA, YC), pp. 1–10.

TAP-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.

QoSA-2014-Meyer #question #trust #verification

Trust or verify? (BM), pp. 1–2.

ASE-2014-UbayashiALLHK #compilation #verification

Abstraction-aware verifying compiler for yet another MDD (NU, DA, PL, YNL, SH, YK), pp. 557–562.

ASE-2014-YangXLCML #adaptation #nondeterminism #self #verification

Verifying self-adaptive applications suffering uncertainty (WY, CX, YL, CC, XM, JL), pp. 199–210.

DAC-2014-SorinMZ #architecture #power management

Architecting Dynamic Power Management to be Formally Verifiable (DJS, OM, MZ), p. 3.

DATE-2014-LeD #design #towards #verification

Towards verifying determinism of SystemC designs (HML, RD), pp. 1–4.

ESOP-2014-BeringerSDA #c #compilation

Verified Compilation for Shared-Memory C (LB, GS, RD, AWA), pp. 107–127.

ESOP-2014-PercontiA #compilation #multi #semantics #using #verification

Verifying an Open Compiler Using Multi-language Semantics (JTP, AA), pp. 128–148.

FASE-2014-Zaharieva-StojanovskiH #concurrent #invariant #source code #verification

Verifying Class Invariants in Concurrent Programs (MZS, MH), pp. 230–245.

TACAS-2014-AngelisFPP #named #source code #verification

VeriMAP: A Tool for Verifying Programs through Transformations (EDA, FF, AP, MP), pp. 568–574.

WRLA-2014-BartolettiMSZ #maude #modelling #verification

Modelling and Verifying Contract-Oriented Systems in Maude (MB, MM, AS, RZ), pp. 130–146.

CSMR-WCRE-2014-MihanceaM #named #security #verification #web

JMODEX: Model extraction for verifying security properties of web applications (PFM, MM), pp. 450–453.

PEPM-2014-CosteaSD #named #verification

HIPimm: verifying granular immutability guarantees (AC, AS, CD), pp. 189–194.

PLDI-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.

PLDI-2014-JagannathanPVPL #compilation #refinement

Atomicity refinement for verified compilation (SJ, GP, JV, DP, VL), p. 5.

PLDI-2014-SampsonPMMGC #probability #verification

Expressing and verifying probabilistic assertions (AS, PP, TM, KSM, DG, LC), p. 14.

SAS-2014-ChenHTWW #recursion #source code #using #verification

Verifying Recursive Programs Using Intraprocedural Analyzers (YFC, CH, MHT, BYW, FW), pp. 118–133.

DLT-2014-YakaryilmazSD #quantum #verification

Debates with Small Transparent Quantum Verifiers (AY, ACCS, HGD), pp. 327–338.

ICALP-v1-2014-Kuncak #recursion #verification

Verifying and Synthesizing Software with Recursive Functions — (Invited Contribution) (VK), pp. 11–25.

FM-2014-ChristakisLS #formal method #verification

Formalizing and Verifying a Modern Build Language (MC, KRML, WS), pp. 643–657.

FM-2014-DerrickDSTTW #consistency #verification

Quiescent Consistency: Defining and Verifying Relaxed Linearizability (JD, BD, GS, BT, OT, HW), pp. 200–214.

FM-2014-GuptaKG #experience #verification

Formally Verifying Graphics FPU — An Intel® Experience (AG, VMAK, RG), pp. 673–687.

FM-2014-LeinoM #automation #induction #proving #verification

Co-induction Simply — Automatic Co-inductive Proofs in a Program Verifier (KRML, MM), pp. 382–398.

IFM-2014-BrideKP #constraints #specification #theorem proving #using #verification #workflow

Verifying Modal Workflow Specifications Using Constraint Solving (HB, OK, FP), pp. 171–186.

IFM-2014-DerrickSD #architecture #verification

Verifying Linearizability on TSO Architectures (JD, GS, BD), pp. 341–356.

IFM-2014-MellerGY #behaviour #uml #verification

Verifying Behavioral UML Systems via CEGAR (YM, OG, KY), pp. 139–154.

SEFM-2014-DiagneMF #verification

A Tool for Verifying Dynamic Properties in B (FD, AM, MF), pp. 290–295.

SEFM-2014-DuboisR #functional #using

Verified Functional Iterators Using the FoCaLiZe Environment (CD, RR), pp. 317–331.

ICGT-2014-PoskittP #graph #higher-order #monad #source code #verification

Verifying Monadic Second-Order Properties of Graph Programs (CMP, DP), pp. 33–48.

HILT-2014-BocchinoGGS #named #programming language

Spot: a programming language for verified flight software (RLB, EG, KPG, RRS), pp. 97–102.

CIKM-2014-CalvaneseMET #modelling #process #uml

Verifiable UML Artifact-Centric Business Process Models (DC, MM, ME, ET), pp. 1289–1298.

SEKE-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.

AMT-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.

MoDELS-2014-ChakiE #compilation #distributed #modelling #verification

Model-Driven Verifying Compilation of Synchronous Distributed Applications (SC, JRE), pp. 201–217.

MoDELS-2014-ChakiE #compilation #distributed #modelling #verification

Model-Driven Verifying Compilation of Synchronous Distributed Applications (SC, JRE), pp. 201–217.

POPL-2014-AmorimCDDHPPPT #architecture #data flow

A verified information-flow architecture (AAdA, NC, AD, DD, CH, DP, BCP, RP, AT), pp. 165–178.

POPL-2014-BouajjaniEH #consistency #replication #verification

Verifying eventual consistency of optimistic replication systems (AB, CE, JH), pp. 285–296.

POPL-2014-KumarMNO #implementation #ml #named

CakeML: a verified implementation of ML (RK, MOM, MN, SO), pp. 179–192.

FSE-2014-LalQ #using #verification

Powering the static driver verifier using corral (AL, SQ), pp. 202–212.

FSE-2014-VakiliD #infinity #modelling #smt #using #verification

Verifying CTL-live properties of infinite state models using an SMT solver (AV, NAD), pp. 213–223.

ICSE-2014-MaozRR #component #modelling #verification

Verifying component and connector models against crosscutting structural views (SM, JOR, BR), pp. 95–105.

HPCA-2014-MatthewsZS #power management

Scalably verifiable dynamic power management (OM, MZ, DJS), pp. 579–590.

CAV-2014-BinghamL #bound #fault #simulation #using #verification

Verifying Relative Error Bounds Using Symbolic Simulation (JB, JLH), pp. 277–292.

CAV-2014-CimattiGMT #hybrid #ltl #verification

Verifying LTL Properties of Hybrid Systems with K-Liveness (AC, AG, SM, ST), pp. 424–440.

CAV-2014-FerraraMNP #data access #named #policy #verification

Vac — Verifier of Administrative Role-Based Access Control Policies (ALF, PM, TLN, GP), pp. 184–191.

CAV-2014-KanavL0 #documentation

A Conference Management System with Verified Document Confidentiality (SK, PL, AP), pp. 167–183.

CAV-2014-RakamaricE #implementation #named #verification

SMACK: Decoupling Source Language Details from Verifier Implementations (ZR, ME), pp. 106–113.

ISSTA-2014-ShachamYGABSV #independence #verification

Verifying atomicity via data independence (OS, EY, GGG, AA, NGB, MS, MTV), pp. 26–36.

VMCAI-2014-AngelisFPP #array #source code #verification

Verifying Array Programs by Transforming Verification Conditions (EDA, FF, AP, MP), pp. 182–202.

VMCAI-2014-DragoiHVWZ #algorithm #framework #verification

A Logic-Based Framework for Verifying Consensus Algorithms (CD, TAH, HV, JW, DZ), pp. 161–181.

ASE-2013-CalinescuJR #self #verification

Developing self-verifying service-based systems (RC, KJ, YR), pp. 734–737.

DAC-2013-LeGHD #simulation #using #verification

Verifying SystemC using an intermediate verification language and symbolic simulation (HML, DG, VH, RD), p. 6.

DATE-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.

PODS-2013-AbouziedAPHS #learning #quantifier #query #verification

Learning and verifying quantified boolean queries by example (AA, DA, CHP, JMH, AS), pp. 49–60.

ESOP-2013-BouajjaniEEH #concurrent #source code #specification #verification

Verifying Concurrent Programs against Sequential Specifications (AB, ME, CE, JH), pp. 290–309.

ESOP-2013-GotsmanRY #algorithm #concurrent #memory management #verification

Verifying Concurrent Memory Reclamation Algorithms with Grace (AG, NR, HY), pp. 249–269.

FASE-2013-GudemannPSD #framework #named #verification

VerChor: A Framework for Verifying Choreographies (MG, PP, GS, AD), pp. 226–230.

FASE-2013-NordioCF #javascript #named #verification

Javanni: A Verifier for JavaScript (MN, CC, CAF), pp. 231–234.

TACAS-2013-PopeeaR #concurrent #contest #multi #named #source code #thread #verification

Threader: A Verifier for Multi-threaded Programs — (Competition Contribution) (CP, AR), pp. 633–636.

PEPM-2013-AngelisFPP #source code #verification

Verifying programs via iterated specialization (EDA, FF, AP, MP), pp. 43–52.

PEPM-2013-CarbinKMR #approximate #program transformation

Verified integrity properties for safe approximate program transformations (MC, DK, SM, MCR), pp. 63–66.

PLDI-2013-GuhaRF #network

Machine-verified network controllers (AG, MR, NF), pp. 483–494.

PLDI-2013-SewellMK #kernel #validation

Translation validation for a verified OS kernel (TALS, MOM, GK), pp. 471–482.

PLDI-2013-SwamyWSCL #higher-order #monad #source code #verification

Verifying higher-order programs with the dijkstra monad (NS, JW, CS, JC, BL), pp. 387–398.

ICALP-v2-2013-DemriDS #complexity #on the #verification

On the Complexity of Verifying Regular Properties on Flat Counter Systems, (SD, AKD, AS), pp. 162–173.

LATA-2013-Etessami #algorithm #infinity #probability #recursion #verification

Algorithms for Analyzing and Verifying Infinite-State Recursive Probabilistic Systems (KE), p. 12.

IFM-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.

SEFM-2013-AmanC #migration #realtime

Real-Time Migration Properties of rTiMo Verified in Uppaal (BA, GC), pp. 31–45.

SEFM-2013-OliveiraJW #csp #multi #protocol

A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP (MVMO, ISdMJ, JW), pp. 46–60.

SEFM-2013-SuryadevaraSMP #behaviour #using #verification

Verifying MARTE/CCSL Mode Behaviors Using UPPAAL (JS, CCS, FM, PP), pp. 1–15.

ICFP-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.

ICFP-2013-TraytelN #regular expression #word

Verified decision procedures for MSO on words based on derivatives of regular expressions (DT, TN), pp. 3–12.

GCM-J-2012-PoskittP #correctness #graph #source code #verification

Verifying Total Correctness of Graph Programs (CMP, DP).

CHI-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.

HIMI-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.

HILT-2013-Taft13a #ada #parallel #programming #set

Bringing safe, dynamic parallel programming to the spark verifiable subset of ada (STT), pp. 37–40.

KDIR-KMIS-2013-AlwazaePK #classification #verification

Verifying the Usefulness of a Classification System of Best Practices (MMSA, EP, HK), pp. 405–412.

OOPSLA-2013-CarbinMR #hardware #reliability #source code #verification

Verifying quantitative reliability for programs that execute on unreliable hardware (MC, SM, MCR), pp. 33–52.

OOPSLA-2013-ShiBH #optimisation #using

Code optimizations using formally verified properties (YS, BB, GH), pp. 427–442.

SAC-2013-MartinaP #induction #multi #protocol #security #using #verification

Verifying multicast-based security protocols using the inductive method (JEM, LCP), pp. 1824–1829.

SAC-2013-MoriguchiW #interactive #reuse #source code

An interactive extension mechanism for reusing verified programs (SM, TW), pp. 1236–1243.

ICSE-2013-Leino #source code

Developing verified programs with dafny (KRML), pp. 1488–1490.

ASPLOS-2013-CuiHWY #execution #symbolic computation #using #verification

Verifying systems rules using rule-directed symbolic execution (HC, GH, JW, JY), pp. 329–342.

ASPLOS-2013-MaiPXKM #invariant #security #verification

Verifying security invariants in ExpressOS (HM, EP, HX, STK, PM), pp. 293–304.

PLOS-2013-FernandezKKA #component #framework #towards

Towards a verified component platform (MF, IK, GK, JA), p. 7.

SOSP-2013-BraunFRSBW #verification

Verifying computations with state (BB, AJF, ZR, STVS, AJB, MW), pp. 341–357.

CADE-2013-HeuleHW #verification

Verifying Refutations with Extended Resolution (MH, WAHJ, NW), pp. 345–359.

CAV-2013-EsparzaLNNSS #execution #ltl #model checking

A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.

DATE-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.

DATE-2012-RajeevMR #architecture #constraints #distributed #embedded #verification

Verifying timing synchronization constraints in distributed embedded architectures (ACR, SM, SR), pp. 200–205.

DATE-2012-YipHI #3d #challenge #design #verification

Challenges in verifying an integrated 3D design (TGY, CYH, VI), pp. 167–168.

ESOP-2012-BartheDP

A Formally Verified SSA-Based Middle-End — Static Single Assignment Meets CompCert (GB, DD, DP), pp. 47–66.

FASE-2012-AlbertBGHR #source code

Verified Resource Guarantees for Heap Manipulating Programs (EA, RB, SG, RH, GRD), pp. 130–145.

FASE-2012-HatvaniPS #adaptation #automaton #embedded #framework #verification

Adaptive Task Automata: A Framework for Verifying Adaptive Embedded Systems (LH, PP, CCS), pp. 115–129.

TACAS-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.

TACAS-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.

TACAS-2012-HolzlN #model checking #verification

Verifying pCTL Model Checking (JH, TN), pp. 347–361.

SCAM-2012-Vidal #execution #symbolic computation #termination #verification

Closed Symbolic Execution for Verifying Program Termination (GV), pp. 34–43.

PLDI-2012-GrebenshchikovLPR #proving #verification

Synthesizing software verifiers from proof rules (SG, NPL, CP, AR), pp. 405–416.

PLDI-2012-LeungGAGJL #gpu #kernel #verification

Verifying GPU kernels by test amplification (AL, MG, YA, RG, RJ, SL), pp. 383–394.

FM-2012-GiorginoS #algorithm #correctness #pointer

Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction (MG, MS), pp. 202–216.

SEFM-2012-ZhuXMQQ #approach #concurrent #source code #verification

The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs (HZ, QX, CM, SQ, ZQ), pp. 172–187.

ICFP-2012-StewartBA #proving #theorem proving

Verified heap theorem prover by paramodulation (GS, LB, AWA), pp. 3–14.

AdaEurope-2012-FairbairnB #implementation #verification

Implementing and Verifying EDF Preemption-Level Resource Control (MLF, AB), pp. 193–206.

HILT-2012-Leino #source code

Developing verified programs with Dafny (KRML), pp. 9–10.

ICEIS-v2-2012-CapelM #approach #automation #composition #correctness #model checking #safety #verification

A Formal Compositional Verification Approach for Safety-Critical Systems Correctness — Model-Checking based Methodological Approach to Automatically Verify Safety Critical Systems Software (MIC, LEMM), pp. 105–112.

ICPR-2012-TaniyamaH #image #recognition #robust

Robust car License Plate Recognition system verified with 163, 574 images captured in fields (KT, KH), pp. 1273–1276.

SEKE-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.

MoDELS-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.

MoDELS-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.

OOPSLA-2012-BettsCDQT #gpu #kernel #named #verification

GPUVerify: a verifier for GPU kernels (AB, NC, AFD, SQ, PT), pp. 113–132.

OOPSLA-2012-LogozzoB #automation #composition #program repair

Modular and verified automatic program repair (FL, TB), pp. 133–146.

OOPSLA-2012-SchillerE #specification

Reducing the barriers to writing verified specifications (TWS, MDE), pp. 95–112.

POPL-2012-LiangFF #concurrent #program transformation #simulation #verification

A rely-guarantee-based simulation for verifying concurrent program transformations (HL, XF, MF), pp. 455–468.

POPL-2012-ZhaoNMZ #formal method #program transformation #representation

Formalizing the LLVM intermediate representation for verified program transformations (JZ, SN, MMKM, SZ), pp. 427–440.

SAC-2012-Affeldt #library #low level #on the

On construction of a library of formally verified low-level arithmetic functions (RA), pp. 1326–1331.

FSE-2012-BeyerHKW #model checking #verification

Conditional model checking: a technique to pass information between verifiers (DB, TAH, MEK, PW), p. 57.

ICSE-2012-AlkhalafBG #analysis #string #using #validation #verification

Verifying client-side input validation functions using string analysis (MA, TB, JLG), pp. 947–957.

ICSE-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.

ICSE-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.

OSDI-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.

CAV-2012-RondonBKJ #c #named #verification

CSolve: Verifying C with Liquid Types (PMR, AB, MK, RJ), pp. 744–750.

ICLP-2012-SchandaB #development #programming #set #using

Using Answer Set Programming in the Development of Verified Software (FS, MB), pp. 72–85.

ICST-2012-MeszarosL #graph transformation

Verified Operational Patterns with Graph Transformation (TM, TL), pp. 954–961.

ICST-2012-SalayCG #towards #verification

Towards a Methodology for Verifying Partial Model Refinements (RS, MC, JG), pp. 938–945.

TAP-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.

TAP-2012-KiniryZH #consistency #library #specification #testing #verification

Testing Library Specifications by Verifying Conformance Tests (JRK, DMZ, RH), pp. 51–66.

VMCAI-2012-CharltonHR #higher-order #named #source code #verification

Crowfoot: A Verifier for Higher-Order Store Programs (NC, BH, BR), pp. 136–151.

VMCAI-2012-OeSOC #named #satisfiability

versat: A Verified Modern SAT Solver (DO, AS, CO, KC), pp. 363–378.

CBSE-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.

ECSA-2011-HamelGKBG #behaviour #transaction #verification

Verifying Composite Service Transactional Behavior with EVENT-B (LH, MG, MK, MTB, WG), pp. 67–74.

DATE-2011-SoekenWD #aspect-oriented #modelling #uml #verification

Verifying dynamic aspects of UML models (MS, RW, RD), pp. 1077–1082.

VLDB-2012-CormodeTY11 #interactive #proving #streaming #verification

Verifying Computations with Streaming Interactive Proofs (GC, JT, KY), pp. 25–36.

ESOP-2011-Appel

Verified Software Toolchain — (Invited Talk) (AWA), pp. 1–17.

PEPM-2011-AlbertBGHPR #using

Verified resource guarantees using COSTA and KeY (EA, RB, SG, RH, GP, GRD), pp. 73–76.

SAS-2011-VafeiadisN #optimisation #verification

Verifying Fence Elimination Optimisations (VV, FZN), pp. 146–162.

FM-2011-BartheBCL #verification

Formally Verifying Isolation and Availability in an Idealized Model of Virtualization (GB, GB, JDC, CL), pp. 231–245.

FM-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.

FM-2011-DerrickSW #verification

Verifying Linearisability with Potential Linearisation Points (JD, GS, HW), pp. 323–337.

FM-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.

FM-2011-LoosPN #adaptation #distributed #hybrid

Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified (SML, AP, LN), pp. 42–56.

SEFM-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.

ICEIS-v3-2011-LinLMZN #approach #verification #workflow

Approach for Verifying Workflow Validity (YL, TL, IM, RZ, RN), pp. 66–75.

KEOD-2011-KhuratS #approach #ontology #policy #verification

An Ontological Approach to Verifying P3P Policies (AK, BS), pp. 349–353.

MoDELS-2011-MoffettBD #consistency #model checking #protocol #uml #using #verification

Verifying UML-RT Protocol Conformance Using Model Checking (YM, AB, JD), pp. 410–424.

MoDELS-2011-MoffettBD #consistency #model checking #protocol #uml #using #verification

Verifying UML-RT Protocol Conformance Using Model Checking (YM, AB, JD), pp. 410–424.

ECOOP-2011-BalzerG #invariant #multi #verification

Verifying Multi-object Invariants with Relationships (SB, TRG), pp. 358–382.

GPCE-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.

POPL-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.

POPL-2011-Leroy #question #tool support

Verified squared: does critical software deserve verified tools? (XL), pp. 1–2.

POPL-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.

POPL-2011-SevcikVNJS #compilation #concurrent

Relaxed-memory concurrency and verified compilation (JS, VV, FZN, SJ, PS), pp. 43–54.

SAC-2011-ChangH #approach #model transformation #multi #using #verification

A model transformation approach for verifying multi-agent systems using SPIN (LC, XH), pp. 37–42.

SAC-2011-MammarFD #approach #reachability #verification

A proof-based approach to verifying reachability properties (AM, MF, FD), pp. 1651–1657.

ICSE-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.

ICSE-2011-CordeiroF #bound #concurrent #model checking #multi #smt #thread #using #verification

Verifying multi-threaded software using smt-based context-bounded model checking (LC, BF), pp. 331–340.

SPLC-2011-GhezziS #approach #model checking #non-functional #parametricity #performance #product line #towards #using #verification

Verifying Non-functional Properties of Software Product Lines: Towards an Efficient Approach Using Parametric Model Checking (CG, AMS), pp. 170–174.

CGO-2011-Leroy #compilation #how #question #verification #why

Formally verifying a compiler: Why? How? How far? (XL).

CAV-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.

CAV-2011-JhalaMR #functional #named #source code #using #verification

HMC: Verifying Functional Programs Using Abstract Interpreters (RJ, RM, AR), pp. 470–485.

LICS-2011-GollerL #complexity #term rewriting #verification

The Complexity of Verifying Ground Tree Rewrite Systems (SG, AWL), pp. 279–288.

SAT-2011-DantsinH #satisfiability

Satisfiability Certificates Verifiable in Subexponential Time (ED, EAH), pp. 19–32.

VMCAI-2011-GotmanovCK #communication #verification

Verifying Deadlock-Freedom of Communication Fabrics (AG, SC, MK), pp. 214–231.

DAC-2010-Coudert #algorithm #performance #verification

An efficient algorithm to verify generalized false paths (OC), pp. 188–193.

DATE-2010-SoekenWKGD #modelling #ocl #satisfiability #uml #using #verification

Verifying UML/OCL models using Boolean satisfiability (MS, RW, MK, MG, RD), pp. 1341–1344.

ESOP-2010-KoprowskiB #interpreter #named #parsing

TRX: A Formally Verified Parser Interpreter (AK, HB), pp. 345–365.

ESOP-2010-Lochbihler #compilation #java #thread #verification

Verifying a Compiler for Java Threads (AL), pp. 427–447.

FASE-2010-KimLK #approach #configuration management #data access #modelling

A Verifiable Modeling Approach to Configurable Role-Based Access Control (DKK, LL, SK), pp. 188–202.

ICSM-2010-KellensNDJP #cobol #design #outsourcing #verification

Verifying the design of an outsourced COBOL system with IntensiVE (AK, CN, TD, LJ, BVP), pp. 1–8.

PLDI-2010-TatlockL #compilation

Bringing extensibility to verified compilers (ZT, SL), pp. 111–121.

SAS-2010-HofmannKS #coq #verification

Verifying a Local Generic Solver in Coq (MH, AK, HS), pp. 340–355.

LATA-2010-SaeedloeiG #induction #realtime #verification

Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R) (NS, GG), pp. 536–548.

IFM-2010-DaumSS #correctness

From Operating-System Correctness to Pervasively Verified Applications (MD, NS, MS), pp. 105–120.

ICFP-2010-ArnoldHKBS #matrix #specification #verification

Specifying and verifying sparse matrix codes (GA, JH, ASK, RB, MS), pp. 249–260.

KEOD-2010-AnjumHY #ontology #verification

Cross Domain Knowledge Verification — Verifying Knowledge in Foundation Ontology based Domain Ontologies (NAA, JAH, BY), pp. 339–342.

MoDELS-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.

ECOOP-2010-StadenCM #execution #logic #object-oriented #specification #verification

Verifying Executable Object-Oriented Specifications with Separation Logic (SvS, CC, BM), pp. 151–174.

ECOOP-2010-SvendsenBP #verification

Verifying Generics and Delegates (KS, LB, MJP), pp. 175–199.

LOPSTR-2010-FioravantiPPS #evaluation #infinity #verification

Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation (FF, AP, MP, VS), pp. 164–183.

POPL-2010-Chlipala #compilation #functional

A verified compiler for an impure functional language (AC), pp. 93–106.

POPL-2010-MalechaMSW #database #relational #towards

Toward a verified relational database management system (JGM, GM, AS, RW), pp. 237–248.

POPL-2010-Myreen #compilation

Verified just-in-time compiler on x86 (MOM), pp. 107–118.

POPL-2010-TristanL #pipes and filters #validation

A simple, verified validator for software pipelining (JBT, XL), pp. 83–92.

ASPLOS-2010-RomanescuLS #consistency #memory management #specification #verification

Specifying and dynamically verifying address translation-aware memory consistency (BFR, ARL, DJS), pp. 323–334.

CC-2010-BurckhardtMS #memory management #modelling #verification

Verifying Local Transformations on Relaxed Memory Models (SB, MM, VS), pp. 104–123.

HPDC-2010-GehaniK #multi #named #trust #verification

Mendel: efficiently verifying the lineage of data modified in multiple trust domains (AG, MK), pp. 227–239.

PPoPP-2010-LiGKQ #source code #verification

A symbolic verifier for CUDA programs (GL, GG, RMK, DQ), pp. 357–358.

CAV-2010-BallBLKL #framework #research #verification

The Static Driver Verifier Research Platform (TB, EB, VL, RK, JL), pp. 119–122.

CAV-2010-CohenNS10a #composition #ltl #named #verification

SPLIT: A Compositional LTL Verifier (AC, KSN, YS), pp. 558–561.

CAV-2010-ConwayB #data type #implementation #low level #verification

Verifying Low-Level Implementations of High-Level Datatypes (CLC, CB), pp. 306–320.

CAV-2010-RepsLTBL #verification

There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code (TWR, JL, AVT, GB, AL), pp. 41–56.

ICST-2010-BruckerBKW #generative #policy #testing

Verified Firewall Policy Transformations for Test Case Generation (ADB, LB, PK, BW), pp. 345–354.

IJCAR-2010-ChaudhuriDLM #proving #safety #verification

Verifying Safety Properties with the TLA+ Proof System (KC, DD, LL, SM), pp. 142–148.

VMCAI-2010-Leino #concurrent #source code #verification

Verifying Concurrent Programs with Chalice (KRML), p. 2.

WICSA-ECSA-2009-BritoRL #architecture #fault tolerance #verification

Verifying architectural variabilities in software fault tolerance techniques (PHSB, CMFR, RdL), pp. 231–240.

ESOP-2009-BarthwalN #execution #parsing

Verified, Executable Parsing (AB, MN), pp. 160–174.

ESOP-2009-LeinoM #concurrent #multi #source code #thread #verification

A Basis for Verifying Multi-threaded Programs (KRML, PM), pp. 378–393.

ESOP-2009-SchaferEM #attribute grammar #coq #formal method #verification

Formalising and Verifying Reference Attribute Grammars in Coq (MS, TE, OdM), pp. 143–159.

TACAS-2009-EmmiJKM #implementation #verification

Verifying Reference Counting Implementations (ME, RJ, EK, RM), pp. 352–367.

CSMR-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.

PLDI-2009-SchwerdfegerW #composition

Verifiable composition of deterministic grammars (AS, EVW), pp. 199–210.

PLDI-2009-TristanL #lazy evaluation #validation

Verified validation of lazy code motion (JBT, XL), pp. 316–326.

SAS-2009-NiedzielskiRGP #bound #constraints #control flow

A Verifiable, Control Flow Aware Constraint Analyzer for Bounds Check Elimination (DN, JvR, AG, KP), pp. 137–153.

CIAA-2009-AtigT #communication #parallel #source code #verification

Verifying Parallel Programs with Dynamic Communication Structures (MFA, TT), pp. 145–154.

LATA-2009-JiraskovaP #automaton #self #verification

Converting Self-verifying Automata into Deterministic Automata (GJ, GP), pp. 458–468.

FM-2009-HarrisKCJR #bound #data flow #process #verification

Verifying Information Flow Control over Unbounded Processes (WRH, NK, SC, SJ, TWR), pp. 773–789.

FM-2009-LarsenLNP #realtime #requirements #verification

Verifying Real-Time Systems against Scenario-Based Requirements (KGL, SL, BN, SP), pp. 676–691.

FM-2009-LeinenbachS #verification

Verifying the Microsoft Hyper-V Hypervisor with VCC (DL, TS), pp. 806–809.

FM-2009-OHalloran #verification

Guess and Verify — Back to the Future (CO), pp. 23–32.

IFM-2009-CabotCR #contract #ocl #uml #verification

Verifying UML/OCL Operation Contracts (JC, RC, DR), pp. 40–55.

SEFM-2009-EzekielL #approach #automation #multi #verification

An Automated Approach to Verifying Diagnosability in Multi-agent Systems (JE, AL), pp. 51–60.

ICFP-2009-KleinDE #case study #experience #kernel #verification

Experience report: seL4: formally verifying a high-performance microkernel (GK, PD, KE), pp. 91–96.

HCI-AUII-2009-DetweilerB #guidelines #online #towards #trust

Trust in Online Technology: Towards Practical Guidelines Based on Experimentally Verified Theory (CD, JB), pp. 605–614.

CAiSE-2009-PlanasCG #action semantics #behaviour #modelling #semantics #specification #uml #verification

Verifying Action Semantics Specifications in UML Behavioral Models (EP, JC, CG), pp. 125–140.

SEKE-2009-SloanKV

An Extendible Translation of BPEL to a Machine-verifiable Model (JCS, TMK, AV), pp. 344–349.

POPL-2009-GantyMR #liveness #source code #verification

Verifying liveness for asynchronous programs (PG, RM, AR), pp. 102–113.

POPL-2009-Ridge #approach #distributed #verification

Verifying distributed systems: the operational approach (TR), pp. 429–440.

SAC-2009-BiagioniDPS #distributed

Practical distributed voter-verifiable secret ballot system (EB, YD, WP, KS), pp. 16–21.

SLE-2009-SchwerdfegerW #composition #parsing

Verifiable Parse Table Composition for Deterministic Parsing (AS, EVW), pp. 184–203.

SPLC-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.

LICS-2009-GollerMT #complexity #on the #process #verification

On the Computational Complexity of Verifying One-Counter Processes (SG, RM, AWT), pp. 235–244.

VMCAI-2009-Vafeiadis #abstraction #verification

Shape-Value Abstraction for Verifying Linearizability (VV), pp. 335–348.

DAC-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.

DAC-2008-KuehlmannBCRMN #verification

Verifying really complex systems: on earth and beyond (AK, AB, DEC, RAR, RMM, AN), pp. 552–553.

DATE-2008-KimSTDV #adaptation #constraints #online #refinement

Constraint Refinement for Online Verifiable Cross-Layer System Adaptation (MK, MOS, CLT, ND, NV), pp. 646–651.

FASE-2008-FantechiGLMPT #approach #model checking #specification #verification

A Model Checking Approach for Verifying COWS Specifications (AF, SG, AL, FM, RP, FT), pp. 230–245.

FASE-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.

TACAS-2008-FismanKL #distributed #fault tolerance #on the #protocol #verification

On Verifying Fault Tolerance of Distributed Protocols (DF, OK, YL), pp. 315–331.

ICALP-C-2008-HallgrenKSZ #protocol #quantum #verification

Making Classical Honest Verifier Zero Knowledge Protocols Secure against Quantum Attacks (SH, AK, PS, SZ), pp. 592–603.

FM-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.

FM-2008-NollR #pointer #thread #verification

Verifying Dynamic Pointer-Manipulating Threads (TN, SR), pp. 84–99.

GT-VMT-2006-NarayananK08 #model transformation #towards #verification

Towards Verifying Model Transformations (AN, GK), pp. 191–200.

GT-VMT-2008-BaresiGMM #abstraction #graph transformation #using #verification

Using Graph Transformation Systems to Specify and Verify Data Abstractions (LB, CG, AM, MM).

GT-VMT-2008-NarayananK #model transformation #verification

Verifying Model Transformations by Structural Correspondence (AN, GK).

SEKE-2008-PengDZ #behaviour #correctness #design pattern #implementation #verification

Verifying Behavioral Correctness of Design Pattern Implementation (TP, JD, YZ), pp. 454–459.

MoDELS-2008-ZamaniKB #enterprise #pattern matching #verification

A Pattern Language Verifier for Web-Based Enterprise Applications (BZ, SK, GB), pp. 553–567.

MoDELS-2008-ZamaniKB #enterprise #pattern matching #verification

A Pattern Language Verifier for Web-Based Enterprise Applications (BZ, SK, GB), pp. 553–567.

OOPSLA-2008-BeckmanBA #type system #verification

Verifying correct usage of atomic blocks and typestate (NEB, KB, JA), pp. 227–244.

GPCE-2008-DenneyF #automation #generative #verification

Generating customized verifiers for automatically generated code (ED, BF), pp. 77–88.

SAC-2008-XuWQ #modelling #using #verification

Modeling and verifying BPEL using synchronized net (CX, HW, WQ), pp. 2358–2362.

SAC-2008-ZuqueteA

Verifiable anonymous vote submission (AZ, FA), pp. 2159–2166.

SPLC-2008-Lutz #consistency #product line

Enabling Verifiable Conformance for Product Lines (RRL), pp. 35–44.

ICST-2008-RamirezC #adaptation #logic #modelling #uml #verification

Verifying and Analyzing Adaptive Logic through UML State Models (AJR, BHCC), pp. 529–532.

ISSTA-2008-LoginovYCFRN #analysis #safety #verification

Verifying dereference safety via expanding-scope analysis (AL, EY, SC, SF, NR, MGN), pp. 213–224.

MBT-2008-BruckerBW #empirical #proving #verification

Verifying Test-Hypotheses: An Experiment in Test and Proof (ADB, LB, BW), pp. 15–27.

ASE-2007-BlancGK #abstraction #c++ #verification

Verifying C++ with STL containers via predicate abstraction (NB, AG, DK), pp. 521–524.

ASE-2007-Leino #specification #verification

Specifying and verifying software (KRML), p. 2.

ESOP-2007-BarthePR #bytecode #java #lightweight #verification

A Certified Lightweight Non-interference Java Bytecode Verifier (GB, DP, TR), pp. 125–140.

ESOP-2007-LeinoS #invariant #using #verification

Using History Invariants to Verify Observers (KRML, WS), pp. 80–94.

TACAS-2007-Leino #challenge #object-oriented #verification

Verifying Object-Oriented Software: Lessons and Challenges (KRML), p. 2.

CSMR-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.

STOC-2007-GoldwasserGHKR #constant #verification

Verifying and decoding in constant depth (SG, DG, AH, TK, GNR), pp. 440–449.

IFM-2007-AguirreRM #community #design #verification

Verifying Temporal Properties of CommUnity Designs (NA, GR, TSEM), pp. 1–20.

IFM-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.

IFM-2007-HanebergGRS #approach #smarttech #verification

Verifying Smart Card Applications: An ASM Approach (DH, HG, WR, GS), pp. 313–332.

SEFM-2007-GrandyBSR #encoding #named #protocol #security

ASN1-light: A Verified Message Encoding for Security Protocols (HG, RB, KS, WR), pp. 195–204.

SEFM-2007-SalehD #approach #novel #security #verification

Verifying Security Properties of Cryptoprotocols: A Novel Approach (MS, MD), pp. 349–360.

SEFM-2007-SchmittT #case study #verification

Verifying the Mondex Case Study (PHS, IT), pp. 47–58.

AGTIVE-2007-AnandK #assembly #generative #graph transformation

Code Graph Transformations for Verifiable Generation of SIMD-Parallel Assembly Code (CKA, WK), pp. 217–232.

SIGAda-2007-LauW #component

Verified component-based software in SPARK: experimental results for a missile guidance system (KKL, ZW), pp. 51–58.

ICEIS-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.

PPDP-2007-BentonZ #compilation #formal method #semantics #verification

Formalizing and verifying semantic type soundness of a simple compiler (NB, UZ), pp. 1–12.

ICSE-2007-Chalin #compilation #evolution #semantics #verification

A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler (PC), pp. 23–33.

CAV-2007-AmitRRSY #abstraction #comparison #verification

Comparison Under Abstraction for Verifying Linearizability (DA, NR, TWR, MS, EY), pp. 477–490.

SAT-2007-Gelder #satisfiability #verification

Verifying Propositional Unsatisfiability: Pitfalls to Avoid (AVG), pp. 328–333.

TAP-2007-BackEM #invariant #source code #testing #verification

Testing and Verifying Invariant Based Programs in the SOCOS Environment (RJB, JE, MM), pp. 61–78.

VMCAI-2007-EmmiM #transaction #verification

Verifying Compensating Transactions (ME, RM), pp. 29–43.

ASE-2006-Futatsugi #proving #specification #verification

Verifying Specifications with Proof Scores in CafeOBJ (KF), pp. 3–10.

DATE-2006-FrehseKR #abstraction #refinement #using #verification

Verifying analog oscillator circuits using forward/backward abstraction refinement (GF, BHK, RAR), pp. 257–262.

FASE-2006-GiorgettiG #generative #ml #named #verification

JAG: JML Annotation Generation for Verifying Temporal Properties (AG, JG), pp. 373–376.

TACAS-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.

ICALP-v2-2006-Vergnaud #verification

New Extensions of Pairing-Based Signatures into Universal Designated Verifier Signatures (DV), pp. 58–69.

FM-2006-Woodcock #challenge

Verified Software Grand Challenge (JW), p. 617.

ICFP-2006-Chlipala #composition #development #proving #verification

Modular development of certified program verifiers with a proof assistant (AC), pp. 160–171.

SOFTVIS-2006-JainCHB #evaluation #java

Experimental evaluation of animated-verifying object viewers for Java (JJ, JHCI, TDH, LAB), pp. 27–36.

SEKE-2006-LeeDSG #approach #modelling #verification

A PVS Approach to Verifying ORA-SS Data Models (SUJL, GD, JS, LG), pp. 126–131.

SEKE-2006-LeeK #architecture #case study #framework #re-engineering #verification

Verifying a Software Architecture Reconstruction Framework with a Case Study (SL, SK), pp. 102–107.

MoDELS-2006-PonsG #ocl #specification #verification

An OCL-Based Technique for Specifying and Verifying Refinement-Oriented Transformations in MDE (CP, DG), pp. 646–660.

MoDELS-2006-PonsG #ocl #specification #verification

An OCL-Based Technique for Specifying and Verifying Refinement-Oriented Transformations in MDE (CP, DG), pp. 646–660.

GPCE-2006-BradyH #compilation #interpreter #staged

A verified staged interpreter is a verified compiler (EB, KH), pp. 111–120.

GPCE-2006-CzarneckiP #constraints #ocl #verification

Verifying feature-based model templates against well-formedness OCL constraints (KC, KP), pp. 211–220.

LOPSTR-2006-MantelSK #data flow #proving #security #verification

Combining Different Proof Techniques for Verifying Information Flow Security (HM, HS, TK), pp. 94–110.

POPL-2006-LahiriQ #verification

Verifying properties of well-founded linked lists (SKL, SQ), pp. 115–126.

POPL-2006-MenonGMMSAP #compilation #optimisation #representation

A verifiable SSA program representation for aggressive compiler optimization (VM, NG, BRM, AM, TS, ARAT, LP), pp. 397–408.

HPCA-2006-ManovitH #consistency #memory management #verification

Completely verifying memory consistency of test program executions (CM, SH), pp. 166–175.

CAV-2006-Hoare

The Ideal of Verified Software (CARH), pp. 5–16.

CAV-2006-KrcalY #automaton #communication #verification

Communicating Timed Automata: The More Synchronous, the More Difficult to Verify (PK, WY), pp. 249–262.

CSL-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.

IJCAR-2006-Chaieb #quantifier #verification

Verifying Mixed Real-Integer Quantifier Elimination (AC), pp. 528–540.

ISSTA-2006-SiegelMAC #execution #model checking #parallel #source code #symbolic computation #using #verification

Using model checking with symbolic execution to verify parallel numerical programs (SFS, AM, GSA, LAC), pp. 157–168.

ASE-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.

ASE-2005-VardhanV #branch #learning #verification

Learning to verify branching time properties (AV, MV), pp. 325–328.

ASE-2005-XuN #approach #modelling #verification

A threat-driven approach to modeling and verifying secure software (DX, KEN), pp. 342–346.

DAC-2005-JainKSC #abstraction #refinement #verification #word

Word level predicate abstraction and refinement for verifying RTL verilog (HJ, DK, NS, EMC), pp. 445–450.

SIGMOD-2005-DeutschMSVZ #data-driven #interactive #verification #web

A Verifier for Interactive, Data-Driven Web Applications (AD, MM, LS, VV, DZ), pp. 539–550.

SIGMOD-2005-PangJRT #query #relational #verification

Verifying Completeness of Relational Query Results in Data Publishing (HP, AJ, KR, KLT), pp. 407–418.

FASE-2005-Berry #design #industrial #performance #specification

Esterel v7: From Verified Formal Specification to Efficient Industrial Designs (GB), p. 1.

TACAS-2005-BouajjaniHMV #model checking #source code #verification

Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking (AB, PH, PM, TV), pp. 13–29.

TACAS-2005-GanaiGA #framework #model checking #named #satisfiability #scalability #verification

DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems (MKG, AG, PA), pp. 575–580.

TACAS-2005-VardhanSVA #using #verification

Using Language Inference to Verify ω-Regular Properties (AV, KS, MV, GA), pp. 45–60.

MSR-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.

PLDI-2005-ElmasTQ #concurrent #detection #named #runtime #source code #verification

VYRD: verifYing concurrent programs by runtime refinement-violation detection (TE, ST, SQ), pp. 27–37.

ICALP-2005-LipmaaWB #security #verification

Designated Verifier Signature Schemes: Attacks, New Security Notions and a New Construction (HL, GW, FB), pp. 459–471.

FM-2005-KatzK #specification #verification

Verifying Scenario-Based Aspect Specifications (EK, SK), pp. 432–447.

FM-2005-SalverdaRZ #parallel #verification

Formally Defining and Verifying Master/Slave Speculative Parallelization (PS, GR, CBZ), pp. 123–138.

SIGAda-2005-NaeserLA #verification

Temporal skeletons for verifying time (GN, KL, LA), pp. 49–56.

SEKE-2005-WangWH #hybrid #linear #verification

Verifying Timed and Linear Hybrid Rule-Systems with RED (FW, RSW, GDH), pp. 448–454.

PPDP-2005-CortierRZ #encryption #protocol #verification

A resolution strategy for verifying cryptographic protocols with CBC encryption and blind signatures (VC, MR, EZ), pp. 12–22.

ICSE-2005-ChinKQPN #alias #policy #safety #verification

Verifying safety policies with size properties and alias controls (WNC, SCK, SQ, CP, HHN), pp. 186–195.

CC-2005-LamKR #consistency #data type #named #verification

Hob: A Tool for Verifying Data Structure Consistency (PL, VK, MCR), pp. 237–241.

PPoPP-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.

SOSP-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.

CAV-2005-BalabanFPZ #invariant #named #verification

IIV: An Invisible Invariant Verifier (IB, YF, AP, LDZ), pp. 408–412.

CAV-2005-ChanderEILN #java #named #verification

JVer: A Java Verifier (AC, DE, NI, PL, GCN), pp. 144–147.

CAV-2005-Yavuz-KahveciBB #verification

Action Language Verifier, Extended (TYK, CB, TB), pp. 413–417.

LICS-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.

VMCAI-2005-AttieC #concurrent #scalability #source code

Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs (PCA, HC), pp. 465–481.

VMCAI-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.

VMCAI-2005-Hoare #challenge #compilation #research #verification

The Verifying Compiler, a Grand Challenge for Computing Research (CARH), p. 78.

ASE-2004-Betin-CanB #concurrent #programming #using

Verifiable Concurrent Programming Using Concurrency Controllers (ABC, TB), pp. 248–257.

ASE-2004-LicataK #interactive #source code #verification #web

Verifying Interactive Web Programs (DRL, SK), pp. 164–173.

DAC-2004-LuJ #using #verification

Verifying a gigabit ethernet switch using SMV (YL, MJ), pp. 230–233.

DAC-2004-ShehataA #composition #verification

A general decomposition strategy for verifying register renaming (HIS, MA), pp. 234–237.

FoSSaCS-2004-GenestMMP #partial order #specification #using #verification

Specifying and Verifying Partial Order Properties Using Template MSCs (BG, MM, AM, DP), pp. 195–210.

PLDI-2004-YahavR #abstraction #safety #using #verification

Verifying safety properties using separation and heterogeneous abstractions (EY, GR), pp. 25–34.

STOC-2004-HolmerinK #equation #linear #verification

A new PCP outer verifier with applications to homogeneous linear equations and max-bisection (JH, SK), pp. 11–20.

IFM-2004-BallCLR #formal method #verification

SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft (TB, BC, VL, SKR), pp. 1–20.

IFM-2004-SchneiderT #component #verification

Verifying Controlled Components (SS, HT), pp. 87–107.

SEFM-2004-EvansTLF #how #information management #verification

How to Verify Dynamic Properties of Information Systems (NE, HT, RL, MF), pp. 416–425.

SIGIR-2004-TsengT #categorisation #verification

Verifying a Chinese collection for text categorization (YHT, WJT), pp. 556–557.

ECOOP-2004-BeersSF #analysis

Efficiently Verifiable Escape Analysis (MQB, CHS, MF), pp. 75–95.

FSE-2004-KrishnamurthiFG #verification

Verifying aspect advice modularly (SK, KF, MG), pp. 137–146.

ICSE-2004-DongLLW #verification

Verifying DAML+OIL and Beyond in Z/EVES (JSD, CHL, YFL, HHW), pp. 201–210.

ICSE-2004-Mariani #behaviour #component #evolution #verification

Behavior Capture and Test for Verifying Evolving Component-Based Systems (LM), pp. 78–80.

LDTA-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.

CAV-2004-BustanRV #markov #verification

Verifying ω-Regular Properties of Markov Chains (DB, SR, MYV), pp. 189–201.

VMCAI-2004-HatcliffRD #concurrent #model checking #object-oriented #specification #using #verification

Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking (JH, R, MBD), pp. 175–190.

ICDAR-2003-MuramatsuM #online #verification

An HMM On-line Signature Verifier Incorporating Signature Trajectories (DM, TM), pp. 438–442.

ESOP-2003-YahavRSW #evolution #logic #verification

Verifying Temporal Heap Properties Specified via Evolution Logic (EY, TWR, SS, RW), pp. 204–222.

TACAS-2003-BozgaLP #abstraction #protocol #verification

Pattern-Based Abstraction for Verifying Secrecy in Protocols (LB, YL, MP), pp. 299–314.

TACAS-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.

FME-2003-Fidge #legacy #verification

Verifying Emulation of Legacy Mission Computer Systems (CJF), pp. 187–207.

SEFM-2003-DeharbeR #debugging #proving #theorem proving #verification

Light-Weight Theorem Proving for Debugging and Verifying Units of Code (DD, SR), pp. 220–228.

SIGAda-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.

SEKE-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-FSE-2003-JeffordsH #requirements #verification

A strategy for efficiently verifying requirements (RDJ, CLH), pp. 28–37.

ESEC-FSE-2003-XieB #component #composition

Verified systems by composition from verified components (FX, JCB), pp. 277–286.

LDTA-2003-Lee #framework

A Formally Verified Register Allocation Framework (KL), pp. 515–531.

CC-2003-Hoare #challenge #compilation #research #verification

The Verifying Compiler: A Grand Challenge for Computing Research (CARH), pp. 262–272.

VMCAI-2003-BossiFPR #bisimulation #security #verification

Bisimulation and Unwinding for Verifying Possibilistic Security Properties (AB, RF, CP, SR), pp. 223–237.

VMCAI-2003-WinEGKL #algorithm #distributed #execution #using #verification

Using Simulated Execution in Verifying Distributed Algorithms (TNW, MDE, SJG, DKK, NAL), pp. 283–297.

CBSE-2003-DijkmanAQ #component #correctness #process #verification

Verifying the Correctness of Component-Based Applications that Support Business Processes (RMD, JAA, DAQ), p. 8.

DAC-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.

DATE-2002-HassounCC #verification

Verifying Clock Schedules in the Presence of Cross Talk (SH, ECG, CC), pp. 346–350.

DATE-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.

PODS-2002-ArenasFL #consistency #on the #specification #verification #xml

On Verifying Consistency of XML Specifications (MA, WF, LL), pp. 259–270.

FoSSaCS-2002-SchoppS #process #using #verification

Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes (US, AKS), pp. 372–386.

WCRE-2002-TanT #fault #program analysis #transaction #verification

Verifying Provisions for Post-Transaction User Input Error Correction through Static Program Analysis (HBKT, NLT), p. 233–?.

STOC-2002-ColeH #verification

Verifying candidate matches in sparse and wildcard matching (RC, RH), pp. 592–601.

FME-2002-ArtsED #case study #erlang #verification

Verifying Erlang Code: A Resource Locker Case-Study (TA, CBE, JD), pp. 184–203.

FME-2002-BackesJP #bisimulation #composition #encryption #implementation #using

Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation (MB, CJ, BP), pp. 310–329.

FME-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.

IFM-2002-XiongCTB

Formally Linking MDG and HOL Based on a Verified MDG System (HX, PC, ST, AB), pp. 205–224.

SEKE-2002-ArandaM #design pattern #formal method #verification

A formal model for verifying compound design patterns (GNA, RM), pp. 213–214.

SEKE-2002-BarbutiTBF #bytecode #java #verification

Fixing the Java bytecode verifier by a suitable type domain (RB, LT, CB, NDF), pp. 377–382.

SEKE-2002-XuVIY #behaviour #modelling #multi #using #verification

Modeling and verifying multi-agent behaviors using predicate/transition nets (DX, RAV, TRI, JY), pp. 193–200.

LOPSTR-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.

FSE-2002-LiKF #verification

Verifying cross-cutting features as open systems (HCL, SK, KF), pp. 89–98.

ICSE-2002-AtiyaK #concurrent #verification

A compliance notation for verifying concurrent systems (DMA, SK), pp. 731–732.

CAV-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.

TestCom-2002-Veciana-NoguesCDS #metric #verification

Verifying IP Meters from Sampled Measurements (CVN, ACA, JDP, JSP), pp. 39–54.

VMCAI-2002-KrsticM #algorithm #monad #verification

Verifying BDD Algorithms through Monadic Interpretation (SK, JM), pp. 182–195.

CBSE-2001-FislerKB #collaboration #component #design #verification

Verifying Component-Based Collaboration Designs (KF, SK, DSB), p. 17.

ASE-2001-BultanY #verification

Action Language Verifier (TB, TYK), pp. 382–386.

ASE-2001-Xia #mobile #verification

Verify Properties of Mobile Code (SX), p. 440.

FASE-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.

FoSSaCS-2001-Nipkow #bytecode #verification

Verified Bytecode Verifiers (TN), pp. 347–363.

STOC-2001-GennaroIKR #complexity #multi

The round complexity of verifiable secret sharing and secure multicast (RG, YI, EK, TR), pp. 580–589.

FME-2001-BurtonKP #implementation #verification

Verifying Implementation Relations (JB, MK, GP), pp. 364–383.

POPL-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.

SAC-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.

ESEC-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.

CAV-2001-AlurW #implementation #network #protocol #refinement #verification

Verifying Network Protocol Implementations by Symbolic Refinement Checking (RA, BYW), pp. 169–181.

CAV-2001-Arons #consistency #using #verification

Using Timestamping and History Variables to Verify Sequential Consistency (TA), pp. 423–435.

CAV-2001-Bertot #formal method #proving #theorem proving #verification

Formalizing a JVML Verifier for Initialization in a Theorem Prover (YB), pp. 14–24.

RTA-2001-KorovinV #order #using #verification

Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order (KK, AV), pp. 137–153.

CBSE-2000-RíoGL #component #named #verification

Itacio: A Component Model for Verifying Software at Construction Time (ACdR, JELG, JMCL), p. 12.

FoSSaCS-2000-BerardLS #equivalence #parallel #performance #process #verification

Verifying Performance Equivalence for Timed Basic Parallel Processes (BB, AL, PS), pp. 35–47.

TACAS-2000-BaukusBLS #network #verification

Abstracting WS1S Systems to Verify Parameterized Networks (KB, SB, YL, KS), pp. 188–203.

TACAS-2000-JonssonN #infinity #transitive #verification

Transitive Closures of Regular Relations for Verifying Infinite-State Systems (BJ, MN), pp. 220–234.

STOC-2000-CramerDD #complexity #multi #on the

On the complexity of verifiable secret sharing and multiparty computation (RC, ID, SD), pp. 325–334.

IFL-2000-ArtsN #erlang #implementation #verification

Verifying Generic Erlang Client-Server Implementations (TA, TN), pp. 37–52.

POPL-2000-VolpanoS #verification

Verifying Secrets and Relative Secrecy (DMV, GS), pp. 268–276.

SAC-2000-DoyonD #bytecode #java #verification

Verifying Object Initialization in the Java Bytecode Language (SD, MD), pp. 821–830.

CAV-2000-Cohen #encryption #first-order #named #protocol #verification

TAPS: A First-Order Verifier for Cryptographic Protocols (EC), pp. 568–571.

CAV-2000-HosabettuGS #architecture #exception #verification

Verifying Advanced Microarchitectures that Support Speculation and Exceptions (RH, GG, MKS), pp. 521–537.

ISSTA-2000-CobleighCO #process #verification

Verifying properties of process definitions (JMC, LAC, LJO), pp. 96–101.

ASE-1999-LiliusP #modelling #named #uml #verification

vUML: A Tool for Verifying UML Models (JL, IP), pp. 255–258.

DAC-1999-AbtsR #multi #scalability #using #verification

Verifying Large-Scale Multiprocessors Using an Abstract Verification Environment (DA, MR), pp. 163–168.

DATE-1999-HendricxC

Formally Verified Redundancy Removal (SH, LJMC), p. 150–?.

DATE-1999-HuhnSKL #verification

Verifying Imprecisely Working Arithmetic Circuits (MH, KS, TK, GL), p. 65–?.

ICDAR-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.

ITiCSE-1999-Kosa #verification #web

Beginners program Web page builders and verifiers (MJK), p. 185.

TACAS-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.

WIA-1999-Trahtman #algorithm #automaton #finite #testing #verification

An Algorithm to Verify Local Threshold Testability of Deterministic Finite Automata (ANT), pp. 164–173.

FM-v1-1999-ArtsD #database #distributed #erlang #verification

Verifying a Distributed Database Lookup Manager Written in Erlang (TA, MD), pp. 682–700.

FM-v1-1999-KestenKPR #analysis #deduction #model checking #verification

A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software (YK, AK, AP, GR), pp. 173–194.

FM-v1-1999-Liu #consistency #specification #testing #verification

Verifying Consistency and Validity of Formal Specifications by Testing (SL), pp. 896–914.

FM-v2-1999-MoriF #behaviour #specification #verification

Verifying Behavioural Specifications in CafeOBJ Environment (AM, KF), pp. 1625–1643.

OOPSLA-1999-FreundM #bytecode #framework #java #verification

A Formal Framework for the Java Bytecode Language and Verifier (SNF, JCM), pp. 147–166.

ICSE-1999-HolzmannS #verification

A Practical Method for Verifying Event-Driven Software (GJH, MHS), pp. 597–607.

CADE-1999-AdamsGLM #named

VSDITLU: a verifiable symbolic definite integral table look-up (AAA, HG, SL, UM), pp. 112–126.

CAV-1999-CimattiCGR #named #verification

NUSMV: A New Symbolic Model Verifier (AC, EMC, FG, MR), pp. 495–499.

CAV-1999-HenzingerQR99a #consistency #multi #verification

Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems (TAH, SQ, SKR), pp. 301–315.

CSL-1999-KestenP #abstraction #liveness #verification

Verifying Liveness by Augmented Abstraction (YK, AP), pp. 141–156.

ASE-1998-OHalloranS #exclamation #verification

Don’t Verify, Abstract! (CO, AS), pp. 53–62.

ESOP-1998-CairesM #concurrent #execution #logic #specification

Verifiable and Executable Logic Specifications of Concurrent Objects in L_pi (LC, LM), pp. 42–56.

TACAS-1998-AbdullaJ #network #process #verification

Verifying Networks of Timed Processes (Extended Abstract) (PAA, BJ), pp. 298–312.

TACAS-1998-Sprenger #calculus #coq #model checking #μ-calculus

A Verified Model Checker for the Modal μ-calculus in Coq (CS), pp. 167–183.

CSMR-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.

STOC-1998-GoldreichSV #statistics

Honest-Verifier Statistical Zero-Knowledge Equals General Statistical Zero-Knowledge (OG, AS, SPV), pp. 399–408.

CAV-1998-FerrariGMPR #mobile #process #verification

Verifying Mobile Processes in the HAL Environment (GLF, SG, UM, MP, GR), pp. 511–515.

CAV-1998-SternD #in memory #memory management #using #verification

Using Magnatic Disk Instead of Main Memory in the Murphi Verifier (US, DLD), pp. 172–183.

CAV-1998-WolperB #infinity #verification

Verifying Systems with Infinite but Regular State Spaces (PW, BB), pp. 88–97.

ISSTA-1998-BultanGL #approach #constraints #integer #verification

Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach (TB, RG, CL), pp. 113–123.

LICS-1998-Alfaro #behaviour #how #probability #verification

How to Specify and Verify the Long-Run Average Behavior of Probabilistic Systems (LdA), pp. 454–465.

ASE-1997-FenselS #architecture #knowledge-based #using #verification

Using KIV to Specify and Verify Architectures of Knowledge-Based Systems (DF, AS), p. 71–?.

TACAS-1997-Prasetya #algorithm #self

Mechanically Verified Self-Stabilizing Hierarchical Algorithms (ISWBP), pp. 399–415.

FME-1997-HemerL #design #pattern matching #reuse

Reuse of Verified Design Templates Through Extended Pattern Matching (DH, PAL), pp. 495–514.

AdaEurope-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.

TRI-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.

ICSE-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.

CAV-1997-Berry #design #verification

Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design (GB), p. 303.

CAV-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.

CAV-1997-PandeyB #evaluation #symmetry #verification

Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation (MP, REB), pp. 244–255.

CAV-1997-SternD #verification

Parallelizing the Murphi Verifier (US, DLD), pp. 256–278.

DAC-1996-Burch #verification

Techniques for Verifying Superscalar Microprocessors (JRB), pp. 552–557.

DAC-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.

PODS-1996-BenediktGL #database #transaction

Verifiable Properties of Database Transactions (MB, TG, LL), pp. 117–127.

TACAS-1996-CleavelandLNS #distributed #modelling #verification

Priorities for Modeling and Verifying Distributed Systems (RC, GL, VN, SS), pp. 278–297.

SAC-1996-Gurr #logic programming #specification

Verifiable partial specifications for logic programming (CAG), pp. 374–379.

CAV-1996-AzizSSB #markov #verification

Verifying Continuous Time Markov Chains (AA, KS, VS, RKB), pp. 269–276.

CAV-1996-CamposG #analysis #model checking #verification

Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System (SVAC, OG), pp. 257–268.

CAV-1996-ClarkeGZ #algorithm #proving #theorem proving #using #verification

Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.

CAV-1996-Gonthier #concurrent #garbage collection #safety #verification

Verifying the Safety of a Practical Concurrent Garbage Collector (GG), pp. 462–465.

CAV-1996-GrafS #invariant #proving #theorem proving #using #verification

Verifying Invariants Using theorem Proving (SG, HS), pp. 196–207.

CAV-1996-Greenstreet #difference #equation #safety #verification

Verifying Safety Properties of Differential Equations (MRG), pp. 277–287.

CAV-1996-IpD #component #verification

Verifying Systems with Replicated Components in Murphi (CNI, DLD), pp. 147–158.

CAV-1996-KapurS #multi #product line #verification

Mechanically Verifying a Family of Multiplier Circuits (DK, MS), pp. 135–146.

PLILP-1995-Fasbender #implementation

A Verified Implementation of Narrowing (HF), pp. 63–80.

PLILP-1995-Hatcliff #correctness #verification

Mechanically Verifying the Correctness of an Offline Partial Evaluator (JH), pp. 279–298.

POPL-1995-BouajjaniEH #composition #infinity #parallel #process #verification

Verifying Infinite State Processes with Sequential and Parallel Composition (AB, RE, PH), pp. 95–106.

ESEC-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.

CAV-1995-BouajjaniR #hybrid #linear #subclass #verification

Verifying ω-Regular Properties for a Subclass of Linear Hybrid Systems (AB, RR), pp. 437–450.

CAV-1995-FidgeKU #realtime #verification

Interactively Verifying a Simple Real-time Scheduler (CJF, PK, MU), pp. 395–408.

CAV-1995-JonssonK #algorithm #distributed #infinity #safety #verification

Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms (BJ, LK), pp. 42–53.

TLCA-1995-Pollack

A Verified Typechecker (RP), pp. 365–380.

DAC-1994-BeattyB #simulation #using #verification

Formally Verifying a Microprocessor Using a Simulation Methodology (DLB, REB), pp. 596–602.

EDAC-1994-KeM #synthesis

Synthesis of Delay-Verifiable Two-Level Circuits (WK, PRM), pp. 297–301.

FME-1994-Evans #concurrent #specification #using #verification

Specifying & Verifying Concurrent Systems Using Z (AE), pp. 366–380.

FME-1994-StoreyH #using

A Strategy for the Production of Verifiable Code Using the B Method (AS, HPH), pp. 346–365.

FSE-1994-DwyerC #analysis #concurrent #data flow #source code #verification

Data Flow Analysis for Verifying Properties of Concurrent Programs (MBD, LAC), pp. 62–75.

ICLP-1994-Diel #towards

Towards a Verified OR-Parallel WAM (SD), pp. 737–738.

SEKE-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.

TOOLS-USA-1993-GlykasWH #design #object-oriented

Verifiable Object Oriented Designs (MG, PW, TH), pp. 391–406.

CAV-1993-Gordon #imperative #source code #verification

A Verifier and Timing Analyser for Simple Imperative Programs (Abstract) (MJCG), p. 320.

CAV-1993-Hungar #model checking #parallel #process #proving #theorem proving #verification

Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.

CAV-1993-JourdanMO #realtime #source code #verification

Verifying Quantitative Real-Time Properties of Synchronous Programs (MJ, FM, AO), pp. 347–358.

CAV-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.

CAV-1993-ProbstL #automaton #behaviour #verification

Verifying Timed Behavior Automata with Input/Output Critical Races (DKP, HFL), pp. 424–437.

CAV-1993-Wilding

A Mechanically Verified Application for a Mechanically Verified Environment (MW), pp. 268–279.

ICALP-1992-SantisPY #bound #proving #statistics #verification

One-Message Statistical Zero-Knowledge Proofs and Space-Bounded Verifier (ADS, GP, MY), pp. 28–40.

CADE-1992-Reif

The KIV System: Systematic Construction of Verified Software (WR), pp. 753–757.

CAV-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.

CAV-1992-Corbett #integer #liveness #programming #safety #verification

Verifying General Safety and Liveness Propterties with Integer Programming (JCC), pp. 357–369.

CAV-1992-De-LeonG #abstraction #composition #distributed #realtime #verification

Modular Abstractions for Verifying Real-Time Distributed Systems (HDL, OG), pp. 2–15.

CAV-1992-ProbstL #automaton #behaviour #constraints #verification

Verifying Timed Behavior Automata with Nonbinary Delay Constraints (DKP, HFL), pp. 123–136.

DAC-1991-Burch #multi #using #verification

Using BDDs to Verify Multipliers (JRB), pp. 408–412.

DAC-1991-BuschV #design #hardware

Proof-Aided Design of Verified Hardware (HB, GV), pp. 391–396.

PEPM-1991-McNerney #abstract interpretation #compilation #correctness #using #verification

Verifying the Correctness of Compiler Transformations on Basic Blocks using Abstract Interpretation (TSM), pp. 106–115.

CAV-1991-GabrielianI #realtime #specification #verification

Verifying Properties of HMS Machine Specifications of Real-Time Systems (AG, RI), pp. 421–431.

CAV-1991-Goldschlag #liveness #safety #verification

Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits (DMG), pp. 354–364.

CAV-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.

PLDI-1990-Giegerich #code generation #on the #specification

On the Structure of Verifiable Code Generator Specifications (RG), pp. 1–8.

PLILP-1990-BowenJP #approach #compilation #prototype #specification

An Approach to Verifiable Compiling Specification and Prototyping (JPB, JH, PKP), pp. 45–59.

CADE-1990-KaflZ #proving #theorem proving #verification

The Theorem Prover of the Program Verifier Tatzelwurm (TK, NZ), pp. 657–658.

CAV-1990-Burch #liveness #safety #verification

Verifying Liveness Properties by Verifying Safety Properties (JRB), pp. 224–232.

CAV-1990-CoudertMB #diagrams #verification

Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams (OC, JCM, CB), pp. 23–32.

CAV-1990-LaiPD #on the #protocol #using #verification

On Using Protean To Verify ISO FTAM Protocol (RL, KRP, TSD), pp. 126–135.

CAV-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.

STOC-1989-Kenyon-MathieuK #partial order #verification

Verifying Partial Orders (CKM, VK), pp. 367–374.

STOC-1989-RabinB #multi #protocol

Verifiable Secret Sharing and Multiparty Protocols with Honest Majority (Extended Abstract) (TR, MBO), pp. 73–85.

LICS-1989-Pfenning #logic #metaprogramming #named

Elf: A Language for Logic Definition and Verified Metaprogramming (FP), pp. 313–322.

TAV-1989-Young #compilation

Verified Compilation in micro-Gypsy (WDY), pp. 20–26.

DAC-1988-WallaceS #named #verification

ATV: An Abstract Timing Verifier (DEW, CHS), pp. 154–159.

ICSE-1988-CraigenKMNPS #named #verification

m-EVES: A Tool for Verifying Software (DC, SK, IM, AN, BP, MS), pp. 324–333.

ICALP-1987-LarsenM #bisimulation #protocol #using #verification

Verifying a Protocol Using Relativized Bisimulation (KGL, RM), pp. 126–135.

ESEC-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.

DAC-1986-GlesnerSS #compilation #named #statistics #verification

SCAT — a new statistical timing verifier in a silicon compiler system (MG, JS, RBS), pp. 220–226.

DAC-1986-OdawaraTOOZ #comparison #logic #verification

A logic verifier based on Boolean comparison (GO, MT, OO, TO, ZqZ), pp. 208–214.

DAC-1986-SupowitF #verification

A new method for verifying sequential circuits (KJS, SJF), pp. 200–207.

DAC-1986-WallaceS #modelling #plugin #verification

Plug-in timing models for an abstract timing verifier (DEW, CHS), pp. 683–689.

CADE-1986-Kafl #linear #reasoning #verification

Program Verifier “Tatzelwurm”: Reasoning about Systems of Linear Inequalities (TK), pp. 300–305.

POPL-1983-Nelson #invariant #reachability #verification

Verifying Reachability Invariants of Linked Structures (GN), pp. 38–47.

DAC-1982-TakashimaMCY #source code #verification

Programs for verifying circuit connectivity of mos/lsi mask artwork (MT, TM, TC, KY), pp. 544–550.

DAC-1980-KoppelmanM #logic #verification

Verifying deep logic hierarchies with ALEX (GMK, KM), pp. 328–335.

POPL-1980-Pratt #on the #specification #verification

On Specifying Verifiers (VRP), pp. 106–116.

DAC-1977-ThomasS #automation #design #performance #verification

Measuring designer performance to verify design automation systems (DET, DPS), pp. 411–418.

ICALP-1976-Cartwright #data type #lisp #source code #verification

User-Defined Data Types as an Aid to Verifying LISP Programs (RC), pp. 228–256.

POPL-1976-GriffithsP #process #specification #verification

Verifying Formal Specifications of Synchronous Processes (PPG, CJP), pp. 192–208.

SOSP-J-1975-OwickiG76 #approach #axiom #parallel #source code #verification

Verifying Properties of Parallel Programs: An Axiomatic Approach (SSO, DG), pp. 279–285.