BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
verification
Google verification

Tag #verification

2955 papers:

POPLPOPL-2020-AbdullaAR
Parameterized verification under TSO is PSPACE-complete (PAA, MFA, RR), p. 29.
POPLPOPL-2020-BartheBGHLPT #c #compilation
Formal verification of a constant-time preserving C compiler (GB, SB, BG, RH, VL, DP, AT), p. 30.
POPLPOPL-2020-ClochardMP #deduction #monitoring
Deductive verification with ghost monitors (MC, CM, AP), p. 26.
POPLPOPL-2020-HarkKGK #bound #induction #probability
Aiming low is harder: induction for lower bounds in probabilistic program verification (MH, BLK, JG, JPK), p. 28.
POPLPOPL-2020-LiuRSGCKY #abstraction #timeline
Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation (ML0, LR, ZS, RG, DC, JEK, MKY), p. 31.
POPLPOPL-2020-SmolkaFHKKS #algebra #linear #source code #testing
Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time (SS, NF, JH, TK, DK, AS0), p. 28.
POPLPOPL-2020-SongCKKKH #composition #lightweight #named
CompCertM: CompCert with C-assembly linking and lightweight modular verification (YS, MC, DK, YK, JK, CKH), p. 31.
POPLPOPL-2020-SozeauBFTW #coq #exclamation #type checking
Coq Coq correct! verification of type checking and erasure for Coq, in Coq (MS, SB, YF0, NT, TW), p. 28.
POPLPOPL-2020-VilhenaPJ #game studies
Spy game: verifying a local generic solver in Iris (PEdV, FP, JHJ), p. 28.
CGOCGO-2020-JoshiFM #approximate #named #reliability #source code
Aloe: verifying reliability of approximate programs in the presence of recovery mechanisms (KJ, VF, SM), pp. 56–67.
CSLCSL-2020-Cortier #protocol #security
Verification of Security Protocols (Invited Talk) (VC), p. 2.
ICSAICSA-2019-GerkingS #architecture #component #cyber-physical #data flow #policy #refinement #security
Component-Based Refinement and Verification of Information-Flow Security Policies for Cyber-Physical Microservice Architectures (CG, DS), pp. 61–70.
FMFM-2019-BeringerA #abstraction #c #composition #source code
Abstraction and Subsumption in Modular Verification of C Programs (LB, AWA), pp. 573–590.
FMFM-2019-BodeveixBCF #liveness #protocol
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol (JPB, JB, DC, MF), pp. 45–63.
FMFM-2019-DerrickDDSW #concurrent #correctness #data type #persistent
Verifying Correctness of Persistent Concurrent Data Structures (JD, SD, BD, GS, HW), pp. 179–195.
FMFM-2019-Evangelidis0
Quantitative Verification of Numerical Stability for Kalman Filters (AE, DP0), pp. 425–441.
FMFM-2019-Lang0M #bisimulation #composition #concurrent
Compositional Verification of Concurrent Systems by Combining Bisimulations (FL, RM0, FM), pp. 196–213.
FMFM-2019-LunelMBT #composition #difference #logic #parallel
Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic (SL, SM, BB, JPT), pp. 354–370.
IFM-2019-ChalupaS #evaluation #slicing
Evaluation of Program Slicing in Software Verification (MC, JS), pp. 101–119.
IFM-2019-HsiehM #automaton #named #protocol
Dione: A Protocol Verification System Built with Dafny for I/O Automata (CH, SM), pp. 227–245.
IFM-2019-LuckcuckFDD0 #specification #summary
A Summary of Formal Specification and Verification of Autonomous Robotic Systems (ML, MF, LAD, CD, MF0), pp. 538–541.
IFM-2019-OortwijnH #abstraction #automation #concurrent #message passing
Practical Abstractions for Automated Verification of Message Passing Concurrency (WO, MH), pp. 399–417.
IFM-2019-OortwijnH19a #industrial #safety
Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System (WO, MH), pp. 418–436.
SEFMSEFM-2019-BeckertBGHLU #relational #slicing #using
Using Relational Verification for Program Slicing (BB, TB, SG, MH, DL, MU), pp. 353–372.
SEFMSEFM-2019-ElderhalliVHKT #fault
Formal Verification of Rewriting Rules for Dynamic Fault Trees (YE, MV0, OH, JPK, ST), pp. 513–531.
SEFMSEFM-2019-FarrellBFDDYM #analysis #case study #using
Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages (MF, MB, MF0, LAD, CD, HY, CM), pp. 471–490.
SEFMSEFM-2019-OliveiraCO #kernel #linux #performance
Efficient Formal Verification for the Linux Kernel (DBdO, TC, RSdO), pp. 315–332.
SEFMSEFM-2019-RingL
Let's Prove It Later - Verification at Different Points in Time (MR, CL), pp. 454–468.
SEFMSEFM-2019-RouxT #bound
Partially Bounded Context-Aware Verification (LLR, CT), pp. 532–548.
SEFMSEFM-2019-WijsW #code generation #composition #concurrent #multi #thread
Modular Indirect Push-Button Formal Verification of Multi-threaded Code Generators (AW, MW), pp. 410–429.
SEFMSEFM-2019-ZhaoOLRFHFPF #health #towards
Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management (XZ, MO, JL, VR, DF, XH0, MF0, FP, AF), pp. 105–124.
HaskellHaskell-2019-ChristiansenDB #coq #haskell #source code
Verifying effectful Haskell programs in Coq (JC, SD, NB), pp. 125–138.
HaskellHaskell-2019-Devriese #approach #case study #composition #haskell #morphism #polymorphism #taxonomy
Modular effects in Haskell through effect polymorphism and explicit dictionary applications: a new approach and the μVeriFast verifier as a case study (DD), pp. 1–14.
HaskellHaskell-2019-MokhovLL #case study #experience #source code
Formal verification of spacecraft control programs (experience report) (AM, GL, JL), pp. 139–145.
ICFP-2019-TimanyB #concurrent #continuation #relational #source code
Mechanized relational verification of concurrent programs with continuations (AT, LB), p. 28.
ECIRECIR-p1-2019-PothaS
Dynamic Ensemble Selection for Author Verification (NP, ES), pp. 102–115.
ECIRECIR-p2-2019-ElsayedNBHSMA #automation #exclamation #identification
CheckThat! at CLEF 2019: Automatic Identification and Verification of Claims (TE, PN, ABC, MH, RS, GDSM, PA), pp. 309–315.
ICMLICML-2019-WengCNSBOD #approach #named #network #probability #robust
PROVEN: Verifying Robustness of Neural Networks with a Probabilistic Approach (LW, PYC, LMN, MSS, AB, IVO, LD), pp. 6727–6736.
MoDELSMoDELS-2019-BesnardTJ0D19a #approach #automaton #modelling #monitoring #uml
Verifying and Monitoring UML Models with Observer Automata: A Transformation-Free Approach (VB, CT, FJ, MB0, PD), pp. 161–171.
OOPSLAOOPSLA-2019-Astrauskas0PS #composition #rust #specification
Leveraging rust types for modular specification and verification (VA, PM0, FP, AJS), p. 30.
OOPSLAOOPSLA-2019-Bastani0S #probability
Probabilistic verification of fairness properties via concentration (OB, XZ0, ASL), p. 27.
OOPSLAOOPSLA-2019-ChenWFBD #learning #relational #using
Relational verification using reinforcement learning (JC, JW, YF, OB, ID), p. 30.
OOPSLAOOPSLA-2019-FernandoJM #approximate #canonical #parallel #safety #source code
Verifying safety and accuracy of approximate parallel programs via canonical sequentialization (VF, KJ, SM), p. 29.
OOPSLAOOPSLA-2019-HamzaVK
System FR: formalized foundations for the stainless verifier (JH, NV, VK), p. 30.
OOPSLAOOPSLA-2019-Huang0CG #composition #probability #source code #termination
Modular verification for almost-sure termination of probabilistic programs (MH, HF0, KC, AKG), p. 29.
OOPSLAOOPSLA-2019-PanchekhaETK #composition #layout #web
Modular verification of web page layout (PP, MDE, ZT, SK), p. 26.
OOPSLAOOPSLA-2019-Ter-GabrielyanS #composition #logic #reachability
Modular verification of heap reachability properties in separation logic (ATG, AJS, PM0), p. 28.
PEPMPEPM-2019-WatanabeTO0 #higher-order #reduction #source code
Reduction from branching-time property verification of higher-order programs to HFL validity checking (KW, TT, HO, NK0), pp. 22–34.
PLDIPLDI-2019-AbdullaAAK #semantics #source code
Verification of programs under the release-acquire semantics (PAA, JA0, MFA, SNK), pp. 1117–1132.
PLDIPLDI-2019-ChajedTKZ #named #refinement
Argosy: verifying layered storage systems with recovery refinement (TC, JT, MFK, NZ), pp. 1054–1068.
PLDIPLDI-2019-ScalasYB #behaviour #message passing #source code
Verifying message-passing programs with dependent behavioural types (AS, NY, EB), pp. 502–516.
PLDIPLDI-2019-SmolkaKKFHK0 #network #probability #scalability
Scalable verification of probabilistic networks (SS, PK0, DMK, NF, JH, DK, AS0), pp. 190–203.
POPLPOPL-2019-GleissenthallKB #distributed #source code
Pretend synchrony: synchronous verification of asynchronous distributed programs (KvG, RGK, AB, DS, RJ), p. 30.
POPLPOPL-2019-MathurMV #decidability #source code
Decidable verification of uninterpreted programs (UM, PM, MV0), p. 29.
POPLPOPL-2019-RaadDRLV #concurrent #consistency #correctness #declarative #library #memory management #modelling #on the #specification
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models (AR, MD, LR, OL, VV), p. 31.
POPLPOPL-2019-SatoABGGH #approximate #convergence #higher-order #optimisation #probability #reasoning #source code
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization (TS, AA0, GB, MG, DG0, JH), p. 30.
PPDPPPDP-2019-0002BMMZ #non-functional
Type-Driven Verification of Non-functional Properties (CB0, ADB, YM, CM, OZ), p. 15.
SASSAS-2019-0001NIU #first-order #fixpoint #logic #source code
Temporal Verification of Programs via First-Order Fixpoint Logic (NK0, TN, AI, HU0), pp. 413–436.
SASSAS-2019-LiLYCHZ #network #performance #precise #towards
Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification (JL, JL, PY, LC, XH0, LZ0), pp. 296–319.
SASSAS-2019-RanzatoZ #robust
Robustness Verification of Support Vector Machines (FR, MZ), pp. 271–295.
SASSAS-2019-YanCSZZX #adaptation #analysis #safety
Per-Dereference Verification of Temporal Heap Safety via Adaptive Context-Sensitive Analysis (HY, SC0, YS, YZ, CZ, JX), pp. 48–72.
SASSAS-2019-YinCL0C #source code #testing
Verifying Numerical Programs via Iterative Abstract Testing (BY, LC, JL, JW0, PC), pp. 247–267.
ASEASE-2019-AfzalACCDDKV #abstraction #generative #testing
VeriAbs : Verification by Abstraction and Test Generation (MA, AA, AC, BC, PD, AD, SK, RV), pp. 1138–1141.
ASEASE-2019-ChittimalliAPMP #framework #named
BuRRiTo: A Framework to Extract, Specify, Verify and Analyze Business Rules (PKC, KA, SP, SM, CP, RS, RN), pp. 1190–1193.
ASEASE-2019-LiuSTWY #c #encryption #source code
Verifying Arithmetic in Cryptographic C Programs (JL, XS, MHT, BYW, BYY), pp. 552–564.
ASEASE-2019-Mudduluru #source code
Verifying Determinism in Sequential Programs (RM), pp. 1271–1273.
ASEASE-2019-Reich #automation #requirements
Inference of Properties from Requirements and Automation of Their Formal Verification (MR), pp. 1222–1225.
ICSE-2019-CabralMSM #evolution #fault #latency #predict
Class imbalance evolution and verification latency in just-in-time software defect prediction (GGC, LLM, ES, SM), pp. 666–676.
ICSE-2019-PanCP0L #modelling #predict
Easy modelling and verification of unpredictable and preemptive interrupt-driven systems (MP, SC, YP0, TZ0, XL), pp. 212–222.
ICSE-2019-Yin0L0 #concurrent #parallel #refinement #thread
Parallel refinement for multi-threaded program verification (LY, WD0, WL, JW0), pp. 643–653.
CASECASE-2019-WasserfallAH #3d
Optical In-Situ Verification of 3D-Printed Electronic Circuits (FW, DA, NH), pp. 1302–1307.
FASEFASE-2019-HuangK #constraints #safety #security
Formal Verification of Safety & Security Related Timing Constraints for a Cooperative Automotive System (LH, EYK0), pp. 210–227.
FASEFASE-2019-QianZWO #c #modelling #named #source code
KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs (JQ, MZ0, YW, KO0), pp. 299–305.
CADECADE-2019-LiT #automation #protocol #proving #security #theorem proving
Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (DLL, AT), pp. 354–365.
CAVCAV-2019-CoenenFST
Verifying Hyperliveness (NC, BF, CS, LT), pp. 121–139.
CAVCAV-2019-FarzanV #automation
Automated Hypersafety Verification (AF, AV), pp. 200–218.
CAVCAV-2019-FengCZF0 #bound #difference #equation
Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations (SF, MC, NZ, MF, BX0), pp. 650–669.
CAVCAV-2019-HongLMR #bisimulation #probability #protocol
Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols) (CDH, AWL, RM, PR), pp. 455–474.
CAVCAV-2019-KatzHIJLLSTWZDK #analysis #framework #network
The Marabou Framework for Verification and Analysis of Deep Neural Networks (GK, DAH, DI, KJ, CL, RL, PS, ST, HW0, AZ, DLD, MJK, CWB), pp. 443–452.
CAVCAV-2019-LangeY #automaton #communication #interactive
Verifying Asynchronous Interactions via Communicating Session Automata (JL, NY), pp. 97–117.
CAVCAV-2019-BerkovitsLLPS #algorithm #composition #decidability #distributed #logic
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics (IB, ML, GL, OP, SS), pp. 245–266.
CAVCAV-2019-GiannarakisBMW #fault tolerance #network #performance #refinement
Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement (NG, RB, RM, DW), pp. 305–323.
CAVCAV-2019-LeeHL #named #optimisation
AliveInLean: A Verified LLVM Peephole Optimization Verifier (JL, CKH, NPL), pp. 445–455.
CAVCAV-2019-LiuWL #source code #using
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (PL, TW, AL), pp. 386–404.
CAVCAV-2019-LiuZWYLLYZ #algorithm #hoare #logic #quantum #using
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic (JL, BZ, SW, SY, TL, YL, MY, NZ), pp. 187–207.
CAVCAV-2019-NagarJ #automation
Automated Parameterized Verification of CRDTs (KN, SJ), pp. 459–477.
ICSTICST-2019-AlthomaliKM #automation #layout #visual notation #web
Automatic Visual Verification of Layout Failures in Responsively Designed Web Pages (IA, GMK, PM), pp. 183–193.
ICSTICST-2019-LegunsenZHRM #runtime
Techniques for Evolution-Aware Runtime Verification (OL, YZ, MHT, GR, DM), pp. 300–311.
TAPTAP-2019-0002JPW #approximate #hardware #question
When Are Software Verification Results Valid for Approximate Hardware? (TI0, MCJ, FP, HW), pp. 3–20.
VMCAIVMCAI-2019-AndreFMS #abstraction #algorithm #industrial #model checking #parametricity #using
Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking (ÉA, LF, JMM, RS), pp. 409–424.
VMCAIVMCAI-2019-BouillaguetBSY #analysis #deduction #in memory #memory management #modelling #pointer
Exploiting Pointer Analysis in Memory Models for Deductive Verification (QB, FB, MS, BY), pp. 160–182.
VMCAIVMCAI-2019-KarlSBM #fault #robust #source code
Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs (AFK, RS, RB, SM), pp. 183–204.
VMCAIVMCAI-2019-NguyenTC #automation #program repair #using
Automatic Program Repair Using Formal Verification and Expression Templates (TTN, QTT, WNC), pp. 70–91.
ICSMEICSME-2018-ChenDZGH #automation #implementation #named #testing
DRLgencert: Deep Learning-Based Automated Testing of Certificate Verification in SSL/TLS Implementations (CC, WD, YZ, SG, CH), pp. 48–58.
ICSMEICSME-2018-SaidQK18a #modelling #state machine
Reflexion Models for State Machine Extraction and Verification (WS, JQ, RK), pp. 149–159.
DLTDLT-2018-0001JJ #automaton #complexity #finite #problem #self
Computational Complexity of Decision Problems on Self-verifying Finite Automata (MH0, SJ, JJJ), pp. 404–415.
FMFM-2018-AlbertGRS0 #modelling #named #source code
SDN-Actors: Modeling and Verification of SDN Programs (EA, MGZ, AR, MS, AS0), pp. 550–567.
FMFM-2018-BergerKAWR #c #case study #experience
Verifying Auto-generated C Code from Simulink - An Experience Report in the Automotive Domain (PB, JPK, , MTBW, TR), pp. 312–328.
FMFM-2018-BeyeneR #integration #tool support
Evidential and Continuous Integration of Software Verification Tools (TAB, HR), pp. 679–685.
FMFM-2018-CimattiST #architecture #specification
Formal Specification and Verification of Dynamic Parametrized Architectures (AC, IS, ST), pp. 625–644.
FMFM-2018-ColvinS #memory management #modelling #source code
A Wide-Spectrum Language for Verification of Programs on Weak Memory Models (RJC, GS), pp. 240–257.
FMFM-2018-KhannaSRP #source code
Dynamic Symbolic Verification of MPI Programs (DK, SS0, CR, RP), pp. 466–484.
FMFM-2018-LetanRCH #composition #coq #source code
Modular Verification of Programs with Effects and Effect Handlers in Coq (TL, YRG, PC, GH), pp. 338–354.
FMFM-2018-NellenRWAK #challenge #empirical #evaluation #modelling #recommendation
Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (JN, TR, MTBW, , JPK), pp. 382–398.
FMFM-2018-Wang0JQX #towards
Towards 'Verifying' a Water Treatment System (JW, JS0, YJ, SQ, ZX), pp. 73–92.
FSCDFSCD-2018-Rosu #design #implementation
Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk) (GR), p. 6.
IFM-2018-BohlenderK #design #industrial
Design and Verification of Restart-Robust Industrial Control Software (DB, SK), pp. 47–68.
IFM-2018-CavalcantiMSL0T #modelling
Modelling and Verification for Swarm Robotics (AC, AM, AS, WL, PR0, JT), pp. 1–19.
IFM-2018-KangMH #constraints #probability #using
Probabilistic Verification of Timing Constraints in Automotive Systems Using UPPAAL-SMC (EYK0, DM, LH), pp. 236–254.
SEFMSEFM-2018-BabaeeGF #framework #learning #predict #runtime #statistics #using
Prevent : A Predictive Run-Time Verification Framework Using Statistical Learning (RB, AG, SF), pp. 205–220.
SEFMSEFM-2018-DinSC #exception #using
Program Verification for Exception Handling on Active Objects Using Futures (CCD, RS, TCC), pp. 73–88.
SEFMSEFM-2018-RashidSH
Formal Verification of Platoon Control Strategies (AR, US, OH), pp. 223–238.
ICFP-2018-BreitnerSLRWW #case study #exclamation #experience #haskell #set
Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report) (JB, ASZ, YL0, CR, JW, SW), p. 16.
ECIRECIR-2018-HalvaniGV
Authorship Verification in the Absence of Explicit Features and Thresholds (OH, LG, IV), pp. 454–465.
ICPRICPR-2018-MingCLVB #detection #interactive #liveness #named #network
FaceLiveNet: End-to-End Networks Combining Face Verification with Interactive Facial Expression-Based Liveness Detection (ZM, JC, MML, MV, JCB), pp. 3507–3512.
ICPRICPR-2018-ShahinJA #approach
One-Class SVMs Based Pronunciation Verification Approach (MAS, JXJ, BA), pp. 2881–2886.
ECMFAECMFA-2018-BaduelCBO #challenge #industrial #modelling #validation
SysML Models Verification and Validation in an Industrial Context: Challenges and Experimentation (RB, MC, JMB, IO), pp. 132–146.
MoDELSMoDELS-2018-BesnardBJTD #embedded #execution #ltl #modelling #uml
Unified LTL Verification and Embedded Execution of UML Models (VB, MB, FJ, CT, PD), pp. 112–122.
OOPSLAOOPSLA-2018-BostonGC #execution #fault tolerance #hardware #modelling #named #programmable
Leto: verifying application-specific hardware fault tolerance with programmable execution models (BB, ZG, MC), p. 30.
OOPSLAOOPSLA-2018-KakiESJ #bound #concurrent #replication
Safe replication through bounded concurrency verification (GK, KE, KCS, SJ), p. 27.
AdaEuropeAdaEurope-2018-JaradatP #contract #design #runtime #safety #using
Using Safety Contracts to Verify Design Assumptions During Runtime (OJ, SP), pp. 3–18.
PEPMPEPM-2018-ImanishiSI #approach
A guess-and-assume approach to loop fusion for program verification (AI, KS, AI), pp. 2–14.
PLDIPLDI-2018-PanchekhaGETK #layout #web
Verifying that web pages have accessible layout (PP, ATG, MDE, ZT, SK), pp. 1–14.
PLDIPLDI-2018-TaubeLMPSSWW #composition #decidability #deduction #distributed
Modularity for decidability of deductive verification with applications to distributed systems (MT, GL, KLM, OP, MS, SS, JRW, DW), pp. 662–677.
POPLPOPL-2018-0001DLC #equivalence
Verifying equivalence of database-driven applications (YW0, ID, SKL, WRC), p. 29.
POPLPOPL-2018-0001ST #higher-order #nondeterminism #refinement #source code #type system
Relatively complete refinement type system for verification of higher-order non-deterministic programs (HU0, YS, TT), p. 29.
POPLPOPL-2018-BurnOR #higher-order #horn clause
Higher-order constrained horn clauses for verification (TCB, CHLO, SJR), p. 28.
POPLPOPL-2018-NguyenGTH #contract #higher-order #source code
Soft contract verification for higher-order stateful programs (PCN, TG, STH, DVH), p. 30.
POPLPOPL-2018-SantosMNWG #javascript #named
JaVerT: JavaScript verification toolchain (JFS, PM, DN, TW0, PG), p. 33.
POPLPOPL-2018-VazouTCSNWJ #refinement #smt
Refinement reflection: complete verification with SMT (NV, AT, VC, RGS, RRN, PW, RJ), p. 31.
PPDPPPDP-2018-Gardner #framework #javascript #named #testing
JaVerT: JavaScript Verification and Testing Framework: Invited Talk (PG), p. 4.
PPDPPPDP-2018-Hanus #declarative #source code
Verifying Fail-Free Declarative Programs (MH), p. 13.
PPDPPPDP-2018-Terao #abstraction #higher-order #lazy evaluation
Lazy Abstraction for Higher-Order Program Verification (TT), p. 13.
SASSAS-2018-HuckelheimLNSH #source code
Verifying Properties of Differentiable Programs (JH, ZL, SHKN, SFS, PDH), pp. 205–222.
SASSAS-2018-MastroeniP #bound
Verifying Bounded Subset-Closed Hyperproperties (IM, MP), pp. 263–283.
SASSAS-2018-McMillanP #decidability #deduction
Deductive Verification in Decidable Fragments with Ivy (KLM, OP), pp. 43–55.
SASSAS-2018-Piskac #synthesis
New Applications of Software Synthesis: Verification of Configuration Files and Firewall Repair (RP), pp. 71–76.
SASSAS-2018-RothenbergDH #abstraction #incremental #using
Incremental Verification Using Trace Abstraction (BCR, DD, MH), pp. 364–382.
SASSAS-2018-Shoham #decidability #distributed #interactive #logic #protocol #using
Interactive Verification of Distributed Protocols Using Decidable Logic (SS), pp. 77–85.
ASEASE-2018-CaoLP #automation #named
L-CMP: an automatic learning-based parameterized verification tool (JC, YL, JP0), pp. 892–895.
ASEASE-2018-ChenH #control flow #smt
Control flow-guided SMT solving for program verification (JC, FH), pp. 351–361.
ESEC-FSEESEC-FSE-2018-0001ZSDR #bytecode #virtual machine
A formal verification tool for Ethereum VM bytecode (DP0, YZ, MS, PD, GR), pp. 912–915.
ESEC-FSEESEC-FSE-2018-LlerenaBBSR #behaviour #modelling #nondeterminism #probability
Verifying the long-run behavior of probabilistic system models in the presence of uncertainty (YRSL, MB, MB, GS, DSR), pp. 587–597.
ESEC-FSEESEC-FSE-2018-YiH #concurrent
Concurrency verification with maximal path causality (QY, JH0), pp. 366–376.
ICSE-2018-BeyerJLW
Reducer-based construction of conditional verifiers (DB0, MCJ, TL0, HW), pp. 1182–1193.
ICSE-2018-LangeNTY #behaviour #framework #message passing #using
A static verification framework for message passing in Go using behavioural types (JL, NN, BT, NY), pp. 1137–1148.
ICSE-2018-YuCWS0
Symbolic verification of regular properties (HY, ZC, JW0, ZS, WD0), pp. 871–881.
GPCEGPCE-2018-Al-SibahiJDW #induction #refinement
Verification of high-level transformations with inductive refinement types (ASAS, TPJ, ASD, AW), pp. 147–160.
ASPLOSASPLOS-2018-TaassoriSB #named #performance
VAULT: Reducing Paging Overheads in SGX with Efficient Integrity Verification Structures (MT, AS, RB), pp. 665–678.
ESOPESOP-2018-0001TW #higher-order #model checking
Higher-Order Program Verification via HFL Model Checking (NK0, TT, KW), pp. 711–738.
ESOPESOP-2018-DoddsBG #compilation #composition #memory management #optimisation
Compositional Verification of Compiler Optimisations on Relaxed Memory (MD, MB, AG), pp. 1027–1055.
ESOPESOP-2018-GueneauCP #complexity #deduction #formal method
A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification (AG, AC, FP), pp. 533–560.
ESOPESOP-2018-MoorePR #induction
Program Verification by Coinduction (BMM, LP, GR), pp. 589–618.
FASEFASE-2018-Marmsoler #design pattern #specification
Hierarchical Specification and Verification of Architectural Design Patterns (DM), pp. 149–168.
CAVCAV-2018-CordeiroKKST #bound #bytecode #java #model checking #named
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (LCC, PK, DK, PS, MT), pp. 183–190.
CAVCAV-2018-Eilers0 #named #python
Nagini: A Static Verifier for Python (ME, PM0), pp. 596–603.
CAVCAV-2018-PickFG #relational #symmetry
Exploiting Synchrony and Symmetry in Relational Verification (LP, GF, AG), pp. 164–182.
CAVCAV-2018-ArndtJKMN #exclamation #graph #java #pointer #source code
Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs (HA, CJ, JPK, CM, TN0), pp. 3–11.
CAVCAV-2018-BouajjaniEJQ #bound #message passing #on the #source code
On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony (AB, CE, KJ, SQ), pp. 372–391.
CAVCAV-2018-ChudnovCCDHMMMM
Continuous Formal Verification of Amazon s2n (AC, NC, BC, JD, BH, CM, SM, EM, EM, ST, AT, EW), pp. 430–446.
CAVCAV-2018-CousotGR #perspective #program analysis
Program Analysis Is Harder Than Verification: A Computability Perspective (PC, RG, FR), pp. 75–95.
CAVCAV-2018-TullsenPCT
Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (MT, LP, NC, AT), pp. 413–429.
CAVCAV-2018-YangVSGM #composition #lazy evaluation #security #self
Lazy Self-composition for Security Verification (WY, YV, PS, AG, SM), pp. 136–156.
CAVCAV-2018-ZhangGSW #named
SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks (JZ, PG, FS, CW0), pp. 157–177.
ICSTICST-2018-PrauseGG #automation #tool support
Evaluating Automated Software Verification Tools (CP, RG, RG), pp. 343–353.
IJCARIJCAR-2018-ZhanH #complexity #imperative #source code
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (BZ, MPLH), pp. 532–548.
TAPTAP-2018-0001DLT #testing #validation
Tests from Witnesses - Execution-Based Validation of Verification Results (DB0, MD, TL0, MT), pp. 3–23.
TAPTAP-2018-BlatterKGPP #c #relational #self
Static and Dynamic Verification of Relational Properties on Self-composed C Code (LB, NK, PLG, VP, GP), pp. 44–62.
TAPTAP-2018-HerdaTB #data flow #dependence #graph #testing #using
Using Dependence Graphs to Assist Verification and Testing of Information-Flow Properties (MH, SST, BB), pp. 83–102.
TAPTAP-2018-Keller #bound #higher-order #testing
Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL (CK), pp. 103–119.
TAPTAP-2018-LeCSW #proving
Verification Coverage for Combining Test and Proof (VHL, LC, JS, VW), pp. 120–138.
TAPTAP-2018-VorobyovKS #c #case study #detection #experience #runtime #security #using
Detection of Security Vulnerabilities in C Code Using Runtime Verification: An Experience Report (KV, NK, JS), pp. 139–156.
VMCAIVMCAI-2018-BaderAT
Gradual Program Verification (JB, JA, ÉT), pp. 25–46.
VMCAIVMCAI-2018-BaumannDMHV #abstraction #automation #source code
Automatic Verification of RMA Programs via Abstraction Extrapolation (CB, AMD, YM, TH, MTV), pp. 47–70.
VMCAIVMCAI-2018-DahiyaB #automation
Automatic Verification of Intermittent Systems (MD, SB), pp. 161–182.
VMCAIVMCAI-2018-Najafzadeh0E #co-evolution #design #file system
Co-Design and Verification of an Available File System (MN, MS0, PE), pp. 358–381.
VMCAIVMCAI-2018-PrabawaALC #composition #data flow #logic
A Logical System for Modular Information Flow Verification (AP, MFAA, BL, WNC), pp. 430–451.
ECSAECSA-2017-CamaraGS #product line #synthesis #trade-off
Synthesis and Quantitative Verification of Tradeoff Spaces for Families of Software Systems (JC, DG, BRS), pp. 3–21.
AFLAFL-2017-MaraisZ #automaton #complexity #difference #self #symmetry
Descriptional Complexity of Non-Unary Self-Verifying Symmetric Difference Automata (LM, LvZ), pp. 157–169.
FSCDFSCD-2017-Gaboardi #higher-order #relational #source code #type system
Type Systems for the Relational Verification of Higher Order Programs (Invited Talk) (MG), p. 1.
IFM-2017-0002MLCT #modelling
Modelling and Verification of Timed Robotic Controllers (PR0, AM, WL, AC, JT), pp. 18–33.
IFM-2017-AronisFS #model checking #testing #using
Testing and Verifying Chain Repair Methods for Corfu Using Stateless Model Checking (SA, SLF, KS), pp. 227–242.
IFM-2017-BeckertBGHLU #automation #named #relational #slicing
SemSlice: Exploiting Relational Verification for Automatic Program Slicing (BB, TB, SG, MH, DL, MU), pp. 312–319.
IFM-2017-BlomDHO #concurrent #parallel #set
The VerCors Tool Set: Verification of Parallel and Concurrent Software (SB, SD, MH, WO), pp. 102–110.
IFM-2017-BruschiPGLP #case study #model checking #protocol #smt
Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study - (DB, ADP, SG, AL, EP), pp. 391–406.
IFM-2017-ChenF #first-order #proving
Triggerless Happy - Intermediate Verification with a First-Order Prover (YC, CAF), pp. 295–311.
IFM-2017-KrishnaPS #automation #named #process
VBPMN: Automated Verification of BPMN Processes (Tool Paper) (AK0, PP, GS), pp. 323–331.
IFM-2017-MoranW #evaluation
Verification of STAR-Vote and Evaluation of FDR and ProVerif (MM, DSW), pp. 422–436.
IFM-2017-PfahlerEBSR #composition
Modular Verification of Order-Preserving Write-Back Caches (JP, GE, SB, GS, WR), pp. 375–390.
IFM-2017-RahmanB #health #recommendation
Formal Verification of CNL Health Recommendations (FR, JKFB), pp. 357–371.
SEFMSEFM-2017-FantechiHM #composition #scalability
Compositional Verification of Interlocking Systems for Large Stations (AF, AEH, HDM), pp. 236–252.
SEFMSEFM-2017-GreinerMB #component #composition #data flow #security
Modular Verification of Information Flow Security in Component-Based Systems (SG, MM, BB), pp. 300–315.
SEFMSEFM-2017-LeildeRTD #framework
A Diagnosis Framework for Critical Systems Verification (Short Paper) (VL, VR, CT, PD), pp. 394–400.
SEFMSEFM-2017-LutebergetCJS #framework #representation
Participatory Verification of Railway Infrastructure by Representing Regulations in RailCNL (BL, JJC, CJ, GS), pp. 87–103.
SEFMSEFM-2017-WiikB #automation #data flow #network #specification
Specification and Automated Verification of Dynamic Dataflow Networks (JW, PB), pp. 136–151.
SEFMSEFM-2017-ZhangRHMC #certification #compilation #industrial
Focused Certification of an Industrial Compilation and Static Verification Toolchain (ZZ, R, JH, YM, PC), pp. 17–34.
HaskellHaskell-2017-VazouLP #coq #haskell #proving #string
A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq (NV, LL, JP), pp. 63–74.
ICFP-2017-ChoiVSCA #composition #framework #hardware #named #parametricity #platform #specification
Kami: a platform for high-level parametric hardware specification and its modular verification (JC, MV, BS, AC, A), p. 30.
ICFP-2017-EbnerURAM #framework #metaprogramming
A metaprogramming framework for formal verification (GE, SU0, JR, JA, LdM), p. 29.
ICFP-2017-OwensNKMT #performance
Verifying efficient function calls in CakeML (SO, MN, RK, MOM, YKT), p. 27.
ICFP-2017-WeitzLHTET #library #named #tool support
SpaceSearch: a library for building and verifying solver-aided tools (KW, SL, SH, ET, MDE, ZT), p. 28.
CIKMCIKM-2017-ZhiSLZ0 #database #named #realtime #using #web
ClaimVerif: A Real-time Claim Verification System Using the Web and Fact Databases (SZ, YS, JL, CZ0, JH0), pp. 2555–2558.
ECMFAECMFA-2017-GogollaHNW #diagrams #independence #uml
Formulating Model Verification Tasks Prover-Independently as UML Diagrams (MG, FH, PN, RW), pp. 232–247.
MoDELSMoDELS-2017-AravantinosK #tool support
Tool Support for Live Formal Verification (VA, SK), pp. 145–155.
MoDELSMoDELS-2017-RamadanS0JG #modelling #process #security
From Secure Business Process Modeling to Design-Level Security Verification (QR, MS, DS, JJ, PG), pp. 123–133.
OOPSLAOOPSLA-2017-AlbarghouthiDDN #named #probability
FairSquare: probabilistic verification of program fairness (AA, LD, SD, AVN), p. 30.
OOPSLAOOPSLA-2017-BakstGKJ #canonical #distributed #source code
Verifying distributed programs via canonical sequentialization (AB, KvG, RGK, RJ), p. 27.
OOPSLAOOPSLA-2017-GomesKMB #consistency #distributed
Verifying strong eventual consistency in distributed systems (VBFG, MK, DPM, ARB), p. 28.
OOPSLAOOPSLA-2017-OrchardCDR #array
Verifying spatial properties of array computations (DAO, MC, MD, ACR), p. 30.
OOPSLAOOPSLA-2017-Swasey0D #composition #robust
Robust and compositional verification of object capability patterns (DS, DG0, DD), p. 26.
LOPSTRLOPSTR-2017-AngelisFPP #abstraction #relational
Predicate Pairing with Abstraction for Relational Verification (EDA, FF, AP, MP), pp. 289–305.
PEPMPEPM-2017-SuwaT0I #code generation #higher-order #model checking
Verification of code generators via higher-order model checking (TS, TT, NK0, AI), pp. 59–70.
POPLPOPL-2017-BouajjaniEGH #consistency #on the
On verifying causal consistency (AB, CE, RG, JH), pp. 626–638.
POPLPOPL-2017-HoenickeMP #composition #concurrent #thread
Thread modularity at many levels: a pearl in compositional verification (JH, RM, AP), pp. 473–485.
POPLPOPL-2017-KonnovLVW #algorithm #distributed #fault tolerance #liveness #safety
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms (IVK0, ML, HV, JW), pp. 719–734.
POPLPOPL-2017-MadhavanKK #contract #higher-order
Contract-based resource verification for higher-order functions with memoization (RM, SK, VK), pp. 330–343.
POPLPOPL-2017-SrikanthSH #complexity #theorem #using
Complexity verification using guided theorem enumeration (AS, BS, WRH), pp. 639–652.
PPDPPPDP-2017-Huisman #parallel #source code
A verification technique for deterministic parallel programs (MH), p. 3.
SASSAS-2017-Albarghouthi #horn clause #probability
Probabilistic Horn Clause Verification (AA), pp. 1–22.
SASSAS-2017-ChakrabortyGU #array #source code
Verifying Array Manipulating Programs by Tiling (SC, AG, DU), pp. 428–449.
SASSAS-2017-GurfinkelN #c #c++ #memory management #source code
A Context-Sensitive Memory Model for Verification of C/C++ Programs (AG, JAN), pp. 148–168.
SASSAS-2017-MastroeniP #framework #semantics
Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification (IM, MP), pp. 232–252.
ASEASE-2017-CelikPG #named #proving #scalability
iCoq: regression proof selection for large-scale verification projects (, KP, MG), pp. 171–182.
ASEASE-2017-CorradiniFP0TV #framework #modelling #named #process
BProVe: a formal verification framework for business process models (FC, FF, AP, BR0, FT, AV), pp. 217–228.
ASEASE-2017-CorradiniFP0TV17a #named #process #tool support
BProVe: tool support for business process verification (FC, FF, AP, BR0, FT, AV), pp. 937–942.
ASEASE-2017-GhassabaniGWHW #metric
Proof-based coverage metrics for formal verification (EG, AG, MWW, MPEH, LGW), pp. 194–199.
ASEASE-2017-MetzlerSBS #concurrent #scheduling #source code
Quick verification of concurrent programs by iteratively relaxed scheduling (PM, HS, PB, NS), pp. 776–781.
ASEASE-2017-SungKW #composition
Modular verification of interrupt-driven software (CS, MK, CW0), pp. 206–216.
ESEC-FSEESEC-FSE-2017-0001RS #compilation
A compiler and verifier for page access oblivious computation (RS0, SKR, SAS), pp. 649–660.
ESEC-FSEESEC-FSE-2017-Easterbrook #how #modelling
Verifying the forecast: how climate models are developed and tested (invited talk) (SE), p. 2.
ESEC-FSEESEC-FSE-2017-TsigkanosKG #cyber-physical #evolution #modelling
Modeling and verification of evolving cyber-physical spaces (CT, TK, CG), pp. 38–48.
ESEC-FSEESEC-FSE-2017-Yu
Practical symbolic verification of regular properties (HY), pp. 1053–1055.
ICSE-2017-BocicB #web
Symbolic model extraction for web application verification (IB, TB), pp. 724–734.
ASPLOSASPLOS-2017-FerraiuoloXZMS #analysis #architecture #data flow #hardware #security
Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis (AF, RX, DZ, ACM, GES), pp. 555–568.
ASPLOSASPLOS-2017-TrippelMLPM #hardware #memory management #named
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA (CT, YAM, DL, MP, MM), pp. 119–133.
ASPLOSASPLOS-2017-ZhangSGCS #identification #security
Identifying Security Critical Properties for the Dynamic Verification of a Processor (RZ, NS, CG, AC, CS), pp. 541–554.
CASECASE-2017-ZitaMF
Application of formal verification to the lane change module of an autonomous vehicle (AZ, SM, MF), pp. 932–937.
ESOPESOP-2017-BouajjaniEEOT #concurrent #robust #source code
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency (AB, ME, CE, BKO, ST), pp. 170–200.
ESOPESOP-2017-Dinsdale-YoungP #automation #concurrent #fine-grained
Caper - Automatic Verification for Fine-Grained Concurrency (TDY, PdRP, KJA, LB), pp. 420–447.
ESOPESOP-2017-Sato0 #composition #functional #higher-order #source code
Modular Verification of Higher-Order Functional Programs (RS, NK0), pp. 831–854.
ESOPESOP-2017-WoodDLE #composition #equivalence #memory management
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation (TW0, SD, SKL, SE), pp. 937–963.
FASEFASE-2017-0002MRSP #component #contract #hybrid
Change and Delay Contracts for Hybrid System Component Verification (AM0, SM, WR, WS, AP), pp. 134–151.
CADECADE-2017-Cruz-FilipeHHKS #performance
Efficient Certified RAT Verification (LCF, MJHH, WAHJ, MK, PSK), pp. 220–236.
CADECADE-2017-PassmoreI #algorithm
Formal Verification of Financial Algorithms (GOP, DI), pp. 26–41.
CADECADE-2017-SantosGMN #javascript #source code #towards
Towards Logic-Based Verification of JavaScript Programs (JFS, PG, PM, DN), pp. 8–25.
CADECADE-2017-TellezB #automation #pointer #proving #source code
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof (GT, JB), pp. 491–508.
CAVCAV-2017-BasinKZ #data type #runtime
Runtime Verification of Temporal Properties over Out-of-Order Data Streams (DAB, FK, EZ), pp. 356–376.
CAVCAV-2017-FanQM0 #composition #data-driven #named #reasoning
DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems (CF, BQ, SM, MV0), pp. 441–461.
CAVCAV-2017-HuangKWW #network #safety
Safety Verification of Deep Neural Networks (XH0, MK, SW, MW), pp. 3–29.
CAVCAV-2017-KatzBDJK #named #network #performance #smt
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (GK, CWB, DLD, KJ, MJK), pp. 97–117.
CAVCAV-2017-Vafeiadis #consistency #logic #memory management #using
Program Verification Under Weak Memory Consistency Using Separation Logic (VV), pp. 30–46.
CAVCAV-2017-WindsorDSP #concurrent #lightweight #named
Starling: Lightweight Concurrency Verification with Views (MW, MD, BS, MJP), pp. 544–569.
CAVCAV-2017-BeameL #integer #towards
Towards Verifying Nonlinear Integer Arithmetic (PB, VL), pp. 238–258.
CAVCAV-2017-GrossmanCIRS #equivalence #source code
Verifying Equivalence of Spark Programs (SG, SC, SI, NR, MS), pp. 282–300.
ICSTICST-2017-ChengT #deduction #incremental #model transformation #relational
Incremental Deductive Verification for Relational Model Transformations (ZC, MT), pp. 379–389.
ICSTICST-2017-DiasFFLSSV #concurrent #contract #source code #using
Verifying Concurrent Programs Using Contracts (RJD, CF0, JF, JML, AS, DGS, TV), pp. 196–206.
ICSTICST-2017-SunRJB #android #named #runtime #using #weaving
ADRENALIN-RV: Android Runtime Verification Using Load-Time Weaving (HS, AR, OJ, WB), pp. 532–539.
ICSTICST-2017-TangCZGXHBM #android #automation #detection #named
NIVAnalyzer: A Tool for Automatically Detecting and Verifying Next-Intent Vulnerabilities in Android Apps (JT, XC, ZZ0, SG, XSX, CH, TB, BM), pp. 492–499.
ICTSSICTSS-2017-GerettiBCGV #automation
Ongoing Work on Automated Verification of Noisy Nonlinear Systems with Ariadne (LG, DB, PC, SZG, TV), pp. 313–319.
ICTSSICTSS-2017-HusterSRKR #robust #testing #using
Using Robustness Testing to Handle Incomplete Verification Results When Combining Verification and Testing Techniques (SH, JS, JR, TK, WR), pp. 54–70.
VMCAIVMCAI-2017-BrideKP #reduction #workflow
Reduction of Workflow Nets for Generalised Soundness Verification (HB, OK, FP), pp. 91–111.
ECSAECSA-2016-Mesli-KesraouiK #architecture #diagrams
Formal Verification of Software-Intensive Systems Architectures Described with Piping and Instrumentation Diagrams (SMK, DK, FO, AB, AT, PB), pp. 210–226.
CSEETCSEET-2016-OkuboNTU #design #development #independence #process #validation
Applying an Instructional Design Process to Development of an Independent Verification and Validation Training Program (NO, KN, ST, YU), pp. 237–240.
ICSMEICSME-2016-LeLLG #automation #deduction #program repair
Enhancing Automated Program Repair with Deductive Verification (XBDL, QLL, DL0, CLG), pp. 428–432.
SCAMSCAM-2016-BlanchardKLL #c #composition #named #parallel #plugin #source code
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs (AB, NK, ML, FL), pp. 67–72.
FMFM-2016-AbdullaAD
Counter-Example Guided Program Verification (PAA, MFA, BPD), pp. 25–42.
FMFM-2016-ChandLS #distributed #multi
Formal Verification of Multi-Paxos for Distributed Consensus (SC, YAL, SDS), pp. 119–136.
FMFM-2016-ChenFLMZ #difference
Validated Simulation-Based Verification of Delayed Differential Dynamics (MC, MF, YL, PNM, NZ), pp. 137–154.
FMFM-2016-ChenP0 #cyber-physical #invariant #learning #towards
Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation (YC0, CMP, JS0), pp. 155–163.
FMFM-2016-GrovLT
Mechanised Verification Patterns for Dafny (GG, YL, VT), pp. 326–343.
FMFM-2016-LetanCHNM #named #security #specification
SpecCert: Specifying and Verifying Hardware-Based Security Enforcement (TL, PC, GH, PN, BM), pp. 496–512.
FMFM-2016-LiSD #automation #protocol #security
Automated Verification of Timed Security Protocols with Clock Drift (LL0, JS0, JSD), pp. 513–530.
FMFM-2016-LiuJZGS #industrial #multi
Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers (HL0, YJ0, HZ, MG0, JS), pp. 764–771.
FMFM-2016-LutebergetJFS #design #incremental #rule-based #tool support
Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations (BL, CJ, CF, MS), pp. 772–778.
FMFM-2016-StrichmanV #recursion
Regression Verification for Unbalanced Recursive Functions (OS, MV), pp. 645–658.
FSCDFSCD-2016-Ahmed #compilation #composition #multi
Compositional Compiler Verification for a Multi-Language World (AA), p. 1.
IFM-2016-AmeriF #why
Why Just Boogie? - Translating Between Intermediate Verification Languages (MA, CAF), pp. 79–95.
IFM-2016-ChenAGSM #behaviour #classification #on the #robust
On Robust Malware Classifiers by Verifying Unwanted Behaviours (WC, DA0, ADG, CAS, IM), pp. 326–341.
IFM-2016-DarvasMV #safety
Formal Verification of Safety PLC Based Control Software (DD, IM, EBV), pp. 508–522.
IFM-2016-FreitasBCW #modelling #runtime
Modelling and Verifying a Priority Scheduler for an SCJ Runtime Environment (LF, JB, AC, AJW), pp. 63–78.
IFM-2016-KumarBLDUB #using
CloudSDV Enabling Static Driver Verifier Using Microsoft Azure (RK, TB, JL, ND, AU, CB), pp. 523–536.
IFM-2016-MullerMRSP #approach #component #hybrid #safety
A Component-Based Approach to Hybrid Systems Safety Verification (AM0, SM, WR, WS, AP), pp. 441–456.
IFM-2016-Preoteasa #invariant #logic #pointer #programming #source code #using
Verifying Pointer Programs Using Separation Logic and Invariant Based Programming in Isabelle (VP), pp. 457–473.
SEFMSEFM-2016-JahnigGG #communication
Refinement-Based Verification of Communicating Unstructured Code (NJ, TG, SG), pp. 61–75.
SEFMSEFM-2016-ZhangQ #coq #framework #implementation #object-oriented
Coq Implementation of OO Verification Framework VeriJ (KZ, ZQ), pp. 270–276.
ICFP-2016-OConnorCRALMNSK #cost analysis #refinement
Refinement through restraint: bringing down the cost of verification (LO, ZC, CR, SA, JL, TCM, YN, TS, GK), pp. 89–102.
CIKMCIKM-2016-LiuLNFTAKVPWMDV #detection #realtime #scalability #twitter
Reuters Tracer: A Large Scale System of Detecting & Verifying Real-Time News Events from Twitter (XL, QL, AN, RF, MT, KA, RK, MV, SP, RW, RM, JD, AV, WK, SS), pp. 207–216.
ICPRICPR-2016-0001PL #correlation #independence
Compact correlated features for writer independent signature verification (AD0, UP0, JL0), pp. 3422–3427.
ICPRICPR-2016-AginakoMSSL #mobile
Local descriptors fusion for mobile iris verification (NA, JMMO, BS, MCS, JLN), pp. 165–169.
ICPRICPR-2016-AhujaIBD #case study
A preliminary study of CNNs for iris and periocular verification in the visible spectrum (KA, RI, FAB, KD), pp. 181–186.
ICPRICPR-2016-HafemannSO #using
Analyzing features learned for Offline Signature Verification using Deep CNNs (LGH, RS, LSO), pp. 2989–2994.
ICPRICPR-2016-HsuCH #representation #using
Object verification in two views using Sparse representation (SCH, ICC, CLH), pp. 504–509.
ICPRICPR-2016-JhuangLT #3d #network #using
Face verification with three-dimensional point cloud by using deep belief networks (DHJ, DTL, CHT), pp. 1430–1435.
ICPRICPR-2016-LuCC #adaptation #metric
Regularized metric adaptation for unconstrained face verification (BL, JCC, RC), pp. 4112–4117.
ICPRICPR-2016-MatsuzakiUSS #2d #3d #constraints #geometry #retrieval #using
Geometric verification using semi-2D constraints for 3D object retrieval (KM, YU, SS, SS), pp. 2338–2343.
ICPRICPR-2016-XuZAC
Template regularized sparse coding for face verification (HX, JZ, AA, RC), pp. 1448–1454.
ICPRICPR-2016-ZhengCBPC
VLAD encoded Deep Convolutional features for unconstrained face verification (JZ, JCC, NB, VMP, RC), pp. 4101–4106.
MoDELSMoDELS-2016-BarnesCVP #communication #industrial #protocol #simulation #towards
Towards the verification of industrial communication protocols through a simulation environment based on QEMU and systemC (CB, JMC, FV, AP), pp. 207–214.
OOPSLAOOPSLA-2016-StefanescuPYLR #semantics
Semantics-based program verifiers for all languages (AS, DP0, SY, YL, GR), pp. 74–91.
OOPSLAOOPSLA-2016-WeitzWTEKT #protocol #scalability #smt
Scalable verification of border gateway protocol configurations with an SMT solver (KW, DW, ET, MDE, AK, ZT), pp. 765–780.
LOPSTRLOPSTR-2016-AngelisFMPP #horn clause #process #using
Verification of Time-Aware Business Processes Using Constrained Horn Clauses (EDA, FF, MCM, AP, MP), pp. 38–55.
PLDIPLDI-2016-0001CLLRSV #design
A design and verification methodology for secure isolated regions (RS0, MC, AL, NPL, SKR, SAS, KV), pp. 665–681.
PLDIPLDI-2016-ChenWSLG #composition #kernel #towards
Toward compositional verification of interruptible OS kernels and device drivers (HC0, X(W, ZS, JL, RG), pp. 431–447.
PLDIPLDI-2016-CostanzoSG #assembly #c #data flow #security #source code
End-to-end verification of information-flow security for C and assembly programs (DC, ZS, RG), pp. 648–664.
PLDIPLDI-2016-GleissenthallBR #quantifier
Cardinalities and universal quantifiers for verifying parameterized systems (KvG, NB, AR), pp. 599–613.
PLDIPLDI-2016-LeeSA #float
Verifying bit-manipulations of floating-point (WL0, RS0, AA), pp. 70–84.
PLDIPLDI-2016-PadonMPSS #interactive #named #safety
Ivy: safety verification by interactive generalization (OP, KLM, AP, MS, SS), pp. 614–630.
PLDIPLDI-2016-ShambaughWG #named
Rehearsal: a configuration verification tool for puppet (RS, AW, AG), pp. 416–430.
PLDIPLDI-2016-SousaD #hoare #logic
Cartesian hoare logic for verifying k-safety properties (MS, ID), pp. 57–69.
POPLPOPL-2016-BaoKPRS #named #source code
PolyCheck: dynamic verification of iteration space transformations on affine programs (WB, SK, LNP, FR, PS), pp. 539–554.
POPLPOPL-2016-KangKHDV #compilation #lightweight
Lightweight verification of separate compilation (JK, YK, CKH, DD, VV), pp. 178–190.
POPLPOPL-2016-MuraseT0SU #functional #higher-order #source code
Temporal verification of higher-order functional programs (AM, TT, NK0, RS, HU0), pp. 57–68.
POPLPOPL-2016-PlotkinBLRV #network #scalability #symmetry #using
Scaling network verification using symmetry and surgery (GDP, NB, NPL, AR, GV), pp. 69–83.
SASSAS-2016-AbdullaJT #automation #policy
Automated Verification of Linearization Policies (PAA, BJ, CQT), pp. 61–83.
SASSAS-2016-AngelisFPP #horn clause #relational
Relational Verification Through Horn Clause Transformation (EDA, FF, AP, MP), pp. 147–169.
SASSAS-2016-MenendezNG #automation #float #named #optimisation
Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM (DM, SN, AG), pp. 317–337.
ASEASE-2016-HentschelHB #empirical #evaluation #interactive #user interface
An empirical evaluation of two user interfaces of an interactive program verifier (MH, RH, RB), pp. 403–413.
ASEASE-2016-HentschelHB16a #comprehension #debugging #effectiveness #interactive #proving
The interactive verification debugger: effective understanding of interactive proof attempts (MH, RH, RB), pp. 846–851.
ASEASE-2016-PavlinovicLS
Inferring annotations for device drivers from verification histories (ZP, AL, RS), pp. 450–460.
ASEASE-2016-YangJGS #approach #automaton
Verifying simulink stateflow model: timed automata approach (YY, YJ, MG, JGS), pp. 852–857.
FSEFSE-2016-BeyerDDH #correctness
Correctness witnesses: exchanging verification results between verifiers (DB, MD, DD, MH), pp. 326–337.
FSEFSE-2016-GurfinkelSM #smt
SMT-based verification of parameterized systems (AG, SS, YM), pp. 338–348.
FSEFSE-2016-JacksonV
Correct or usable? the limits of traditional verification (impact paper award) (DJ0, MV), p. 11.
ICSE-2016-ChenHLLTWW #synthesis
PAC learning-based verification and model synthesis (YFC, CH, OL, TJL, MHT, BYW, FW), pp. 714–724.
ASPLOSASPLOS-2016-AmaniHCRCOBNLST #file system #implementation #named
CoGENT: Verifying High-Assurance File System Implementations (SA, AH, ZC, CR, PC, LO, JB, YN, JL, TS, JT, GK, TCM, GK, GH), pp. 175–188.
ASPLOSASPLOS-2016-LustigSMB #interface #memory management #named
COATCheck: Verifying Memory Ordering at the Hardware-OS Interface (DL, GS, MM, AB), pp. 233–247.
CASECASE-2016-HamanaAX #approach #information management #petri net
A timed Petri net approach for verification of Territorial Healthcare Information Systems (SH, VA, XX), pp. 658–663.
ESOPESOP-2016-LourencoFP #adaptation #approach #formal method
Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach (CBL, MJF, JSP), pp. 41–67.
ESOPESOP-2016-PintoDGS #composition #concurrent #termination
Modular Termination Verification for Non-blocking Concurrency (PdRP, TDY, PG, JS), pp. 176–201.
ESOPESOP-2016-Summers0 #composition #message passing #source code
Actor Services - Modular Verification of Message Passing Programs (AJS, PM0), pp. 699–726.
FASEFASE-2016-HenrioKLM #component #distributed #ide
Integrated Environment for Verifying and Running Distributed Components (LH, OK, SL, EM), pp. 66–83.
FASEFASE-2016-HuY #api #generative #hybrid
Hybrid Session Verification Through Endpoint API Generation (RH, NY), pp. 401–418.
FASEFASE-2016-LechenetKG #branch #debugging #slicing
Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices (JCL, NK, PLG), pp. 179–196.
FASEFASE-2016-PutterW #automaton #correctness #lts
Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique (SdP, AW), pp. 383–400.
CAVCAV-2016-Duggirala0 #linear #simulation
Parsimonious, Simulation Based Verification of Linear Systems (PSD, MV0), pp. 477–494.
CAVCAV-2016-HeMW
Learning-Based Assume-Guarantee Regression Verification (FH0, SM, BYW), pp. 310–328.
CAVCAV-2016-KafleGM #abstract interpretation #automaton #finite #horn clause #named #using
Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata (BK, JPG, JFM), pp. 261–268.
CAVCAV-2016-KahsaiRSS #framework #java #named #source code
JayHorn: A Framework for Verifying Java programs (TK, PR, HS, MS), pp. 352–358.
CAVCAV-2016-LeinoP
Trigger Selection Strategies to Stabilize Program Verifiers (KRML, CPC), pp. 361–381.
CAVCAV-2016-MuellerSS #automation #execution #symbolic computation #using
Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution (PM, MS, AJS), pp. 405–425.
CAVCAV-2016-NgoLJ #modelling #named #probability #runtime
PSCV: A Runtime Verification Tool for Probabilistic SystemC Models (VCN, AL, VJ), pp. 84–91.
CAVCAV-2016-ReidCDGHKPSVZ
End-to-End Verification of Processors with ISA-Formal (AR, RC, AD, DG, DH, WK, AP, OS, PV, AZ), pp. 42–58.
CAVCAV-2016-XuFFZZL #framework #kernel
A Practical Verification Framework for Preemptive OS Kernels (FX, MF, XF, XZ, HZ, ZL), pp. 59–79.
ICSTICST-2016-Gustavsson
Verification Methodology for Fully Autonomous Heavy Vehicles (JG), pp. 381–382.
IJCARIJCAR-2016-AthanasiouLW #bound #equation #thread #using
Unbounded-Thread Program Verification using Thread-State Equations (KA, PL, TW), pp. 516–531.
TAPTAP-2016-GabmeyerS #graph transformation #hardware #lightweight #model checking #off the shelf
Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers (SG, MS), pp. 94–111.
TAPTAP-2016-Liu #specification #testing #theorem
Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification (SL), pp. 112–129.
TAPTAP-2016-ReichlFT #formal method #using #validation
Using Formal Methods for Verification and Validation in Railway (KR, TF, PT), pp. 3–13.
VMCAIVMCAI-2016-0001SS #framework #named #reasoning
Viper: A Verification Infrastructure for Permission-Based Reasoning (PM0, MS, AJS), pp. 41–62.
VMCAIVMCAI-2016-Holzmann #concurrent
Cloud-Based Verification of Concurrent Software (GJH), pp. 311–327.
ICSMEICSME-2015-MedicherlaKN #specification #using
Program specialization and verification using file format specifications (RKM, RK, SN), pp. 191–200.
LATALATA-2015-FarzanHHKP #automation
Automated Program Verification (AF, MH, JH, ZK, AP), pp. 25–46.
FMFM-2015-AhrendtCPS #runtime #specification
A Specification Language for Static and Runtime Verification of Data and Control Properties (WA, JMC, GJP, GS), pp. 108–125.
FMFM-2015-AlTurkiA #distributed #framework #towards #using #𝕂
Towards Formal Verification of Orchestration Computations Using the 𝕂 Framework (MAA, OA), pp. 40–56.
FMFM-2015-BagheriKMJ #android #bound #design #detection #protocol
Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification (HB, EK, SM, DJ), pp. 73–89.
FMFM-2015-BratBDGHK #safety
Verifying the Safety of a Flight-Critical System (GB, DHB, MD, DG, FH, TK), pp. 308–324.
FMFM-2015-Damm #analysis #automation #lessons learnt #named
AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned (WD), pp. 18–19.
FMFM-2015-DerrickDSTW #transaction
Verifying Opacity of a Transactional Mutex Lock (JD, BD, GS, OT, HW), pp. 161–177.
FMFM-2015-FernandezAKK #automation
Automated Verification of RPC Stub Code (MF, JA, GK, IK), pp. 273–290.
FMFM-2015-Lecomte #modelling
Formal Virtual Modelling and Data Verification for Supervision Systems (TL), pp. 597–600.
FMFM-2015-LiSLD #protocol #security
Verifying Parameterized Timed Security Protocols (LL, JS, YL, JSD), pp. 342–359.
FMFM-2015-MirandaMR #automation #design #generative #testing #using
Using Simulink Design Verifier for Automatic Generation of Requirements-Based Tests (BM, HM, RR), pp. 601–604.
FMFM-2015-SogokonJ #hybrid #liveness
Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems (AS, PBJ), pp. 514–531.
SEFMSEFM-2015-AmighiDBH #source code #specification
Specification and Verification of Atomic Operations in GPGPU Programs (AA, SD, SB, MH), pp. 69–83.
SEFMSEFM-2015-BlomHZ #behaviour #concurrent #functional #source code
History-Based Verification of Functional Behaviour of Concurrent Programs (SB, MH, MZS), pp. 84–98.
SEFMSEFM-2015-ClarisoGC #bound #ocl #refinement #towards #uml
Towards Domain Refinement for UML/OCL Bounded Verification (RC, CAG, JC), pp. 108–114.
SEFMSEFM-2015-ColomboDF #runtime
Investigating Instrumentation Techniques for ESB Runtime Verification (CC, GD, AF), pp. 99–107.
SEFMSEFM-2015-Muhlberg0DLP #learning #source code
Learning Assertions to Verify Linked-List Programs (JTM, DHW, MD, GL, FP), pp. 37–52.
SEFMSEFM-2015-Vanspauwen0 #encryption #implementation #library #protocol #specification
Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications (GV, BJ), pp. 53–68.
GaMGaM-2015-HeussnerPCM #concurrent #graph #object-oriented #towards
Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model (AH, CMP, CC, BM), pp. 32–47.
ICGTICGT-2015-KwantesGKR #modelling #process #towards
Towards Compliance Verification Between Global and Local Process Models (PMK, PVG, JK, AR), pp. 221–236.
ICGTICGT-2015-Stuckrath #analysis #graph transformation #named #using
Uncover: Using Coverability Analysis for Verifying Graph Transformation Systems (JS), pp. 266–274.
HCIDUXU-UI-2015-HwangLJ #difference #gender #smarttech #user interface #women
Verification of Stereotype on Women Observing Gender Difference on UX of Wearable Device (HJH, JML, DYJ), pp. 214–223.
CAiSECAiSE-2015-DelmasP #policy #requirements
Need-to-Share and Non-diffusion Requirements Verification in Exchange Policies (RD, TP), pp. 151–165.
CAiSECAiSE-2015-EstanolST #modelling #process #uml #validation
Verification and Validation of UML Artifact-Centric Business Process Models (ME, MRS, ET), pp. 434–449.
ICEISICEIS-v3-2015-PassosJ #process #workflow
Relaxed Soundness Verification for Interorganizational Workflow Processes (LMSP, SJ), pp. 221–228.
SEKESEKE-2015-LiuH #petri net #pipes and filters
PIPE+Verifier — A Tool for Analyzing High Level Petri Nets (SL, XH), pp. 575–580.
SEKESEKE-2015-XiangQB #flexibility #java #runtime
Flexible and Extensible Runtime Verification for Java (CX, ZQ, WB), pp. 595–600.
ECMFAECMFA-J-2012-BaresiBKMMPRR15 #approach #embedded #uml #validation
Formal verification and validation of embedded systems: the UML-based MADES approach (LB, GB, DSK, NDM, AM, RFP, AR, MR), pp. 343–363.
AMTAMT-2015-DyckGLSG #automation #behaviour #model transformation #towards
Towards the Automatic Verification of Behavior Preservation at the Transformation Level for Operational Model Transformations (JD, HG, LL, SS, SG), pp. 36–45.
AMTAMT-2015-SelimCDLO #case study #debugging #experience #model transformation
Finding and Fixing Bugs in Model Transformations with Formal Verification: An Experience Report (GMKS, JRC, JD, LL, BJO), pp. 26–35.
ICMTICMT-2015-HilkenNGW #concept #modelling #ocl #uml #validation
From UML/OCL to Base Models: Transformation Concepts for Generic Validation and Verification (FH, PN, MG, RW), pp. 149–165.
MoDELSMoDELS-2015-OakesTLW #atl #contract #declarative
Fully verifying transformation contracts for declarative ATL (BJO, JT, LL, MW), pp. 256–265.
ECOOPECOOP-2015-BostromM #composition #finite #source code
Modular Verification of Finite Blocking in Non-terminating Programs (PB, PM), pp. 639–663.
ECOOPECOOP-2015-JacobsBK #composition #termination
Modular Termination Verification (BJ, DB, RK), pp. 664–688.
ECOOPECOOP-2015-SchwerhoffS #automation #lightweight
Lightweight Support for Magic Wands in an Automatic Verifier (MS, AJS), pp. 614–638.
ECOOPECOOP-2015-Summers #stack
Software Verification “Across the Stack” (AJS), p. 3.
ECOOPECOOP-2015-VekrisCJ #trust #type system
Trust, but Verify: Two-Phase Typing for Dynamic Languages (PV, BC, RJ), pp. 52–75.
OOPSLAOOPSLA-2015-BastaniAA #android #data flow
Interactively verifying absence of explicit information flows in Android apps (OB, SA, AA), pp. 299–315.
OOPSLAOOPSLA-2015-LopezMMNSVY #message passing #parallel #source code
Protocol-based verification of message-passing parallel programs (HAL, ERBM, FM, NN, CS, VTV, NY), pp. 280–298.
PLATEAUPLATEAU-2015-Pearce #usability
Some usability hypotheses for verification (DJP), pp. 57–60.
LOPSTRLOPSTR-2015-MontenegroPS #generative #representation
A Generic Intermediate Representation for Verification Condition Generation (MM, RP, JSH), pp. 227–243.
PEPMPEPM-2015-AsadaS0 #first-order #functional #refinement #relational #source code
Verifying Relational Properties of Functional Programs by First-Order Refinement (KA, RS, NK), pp. 61–72.
PEPMPEPM-2015-KafleG #constraints #horn clause
Constraint Specialisation in Horn Clause Verification (BK, JPG), pp. 85–90.
PEPMPEPM-2015-LeCT #concurrent #thread
Threads as Resource for Concurrency Verification (DKL, WNC, YMT), pp. 73–84.
PLDIPLDI-2015-Appel #encryption
Verification of a cryptographic primitive: SHA-256 (AWA), p. 153.
PLDIPLDI-2015-SergeyNB #concurrent #fine-grained #source code
Mechanized verification of fine-grained concurrent programs (IS, AN, AB), pp. 77–87.
PLDIPLDI-2015-SharmaBA #gpu #source code
Verification of producer-consumer synchronization in GPU programs (RS, MB, AA), pp. 88–98.
PLDIPLDI-2015-TassarottiDV #logic #memory management
Verifying read-copy-update in a logic for weak memory (JT, DD, VV), pp. 110–120.
PLDIPLDI-2015-WilcoxWPTWEA #distributed #framework #implementation #named
Verdi: a framework for implementing and formally verifying distributed systems (JRW, DW, PP, ZT, XW, MDE, TEA), pp. 357–368.
POPLPOPL-2015-Agten0P #c #composition
Sound Modular Verification of C Code Executing in an Unverified Context (PA, BJ, FP), pp. 581–594.
POPLPOPL-2015-Chlipala15a #case study #composition #interface #network #parallel #thread #web
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification (AC), pp. 609–622.
PPDPPPDP-2015-Al-HumaimeedyF #multi #specification
Enhancing the specification and verification techniques of multiparty sessions in SOC (ASAH, MF), pp. 19–30.
PPDPPPDP-2015-AngelisFPP #generative #semantics
Semantics-based generation of verification conditions by program specialization (EDA, FF, AP, MP), pp. 91–102.
PPDPPPDP-2015-ChenLJZL #automation #declarative #network #safety #source code
Automated verification of safety properties of declarative networking programs (CC, LKL, LJ, WZ, BTL), pp. 79–90.
PPDPPPDP-2015-Cousot #abstract interpretation #induction
Verification by abstract interpretation, soundness and abstract induction (PC), pp. 1–4.
SASSAS-2015-Brain0KS #invariant #safety
Safety Verification and Refutation by k-Invariants and k-Induction (MB, SJ, DK, PS), pp. 145–161.
SASSAS-2015-Terauchi #effectiveness #heuristic #refinement
Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR (TT), pp. 128–144.
ASEASE-2015-BocicB #logic #performance
Efficient Data Model Verification with Many-Sorted Logic (T) (IB, TB), pp. 42–52.
ASEASE-2015-GroceAJM #how
How Verified is My Code? Falsification-Driven Verification (T) (AG, IA, CJ, PEM), pp. 737–748.
ASEASE-2015-LinSNLD #composition
Interpolation Guided Compositional Verification (T) (SWL, JS, TKN, YL, JSD), pp. 65–74.
ASEASE-2015-TomanPT #bound #named #rust
Crust: A Bounded Verifier for Rust (N) (JT, SP, ET), pp. 75–80.
ASEASE-2015-ZhengRLDS #named #parallel #source code
CIVL: Formal Verification of Parallel Programs (MZ, MSR, ZL, MBD, SFS), pp. 830–835.
ESEC-FSEESEC-FSE-2015-0001DDHS #validation
Witness validation and stepwise testification across software verifiers (DB, MD, DD, MH, AS), pp. 721–733.
ICSEICSE-v1-2015-BaresiKR #ltl #performance #scalability #specification
Efficient Scalable Verification of LTL Specifications (LB, MMPK, MR), pp. 711–721.
ICSEICSE-v1-2015-BocicB #performance
Coexecutability for Efficient Verification of Data Model Updates (IB, TB), pp. 744–754.
ICSEICSE-v1-2015-MatichukMAJKS #empirical #formal method #towards
Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification (DM, TCM, JA, DRJ, GK, MS), pp. 722–732.
ICSEICSE-v2-2015-Kallehbasti #modelling #scalability #uml
Scalable Formal Verification of UML Models (MMPK), pp. 847–850.
ICSEICSE-v2-2015-Merwe #android
Verification of Android Applications (HvdM), pp. 931–934.
SACSAC-2015-DiazCMR #architecture #model checking #web #web service
Model-checking verification of publish-subscribe architectures in web service contexts (GD, MEC, HM, VVR), pp. 1688–1695.
SACSAC-2015-KhelladiBBLG #consistency #framework #process
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
Verifying eventuality properties of imprecise system requirements using event-B (HAL, NTT, SN), pp. 1651–1653.
ASPLOSASPLOS-2015-FletcherRKDD #ram #recursion
Freecursive ORAM: [Nearly] Free Recursion and Integrity Verification for Position-based Oblivious RAM (CWF, LR, AK, MvD, SD), pp. 103–116.
CASECASE-2015-AicherRV #abstraction #automation #simulation #towards
Towards finding the appropriate level of abstraction to model and verify automated production systems in discrete event simulation (TA, SR, BVH), pp. 1048–1053.
CASECASE-2015-JiangDZZ #formal method #mobile #modelling
Formal modeling and verification of secure mobile agent systems (MJ, ZD, MZ, YZ), pp. 545–550.
CASECASE-2015-Malik #composition
Advanced selfloop removal in compositional nonblocking verification of discrete event systems (RM), pp. 819–824.
CCCC-2015-DemangePS #coq #optimisation #performance
Verifying Fast and Sparse SSA-Based Optimizations in Coq (DD, DP, LS), pp. 233–252.
DACDAC-2015-AsadJ #programming #using
Verifying inevitability of phase-locking in a charge pump phase lock loop using sum of squares programming (HuA, KDJ), p. 6.
DACDAC-2015-CiesielskiYBLR
Verification of gate-level arithmetic circuits by function extraction (MJC, CY, WB, DL, AR), p. 6.
DACDAC-2015-EspinosaHAAR #analysis #correlation #robust #set
Analysis and RTL correlation of instruction set simulators for automotive microcontroller robustness verification (JE, CH, JA, DdA, JCR), p. 6.
DACDAC-2015-Foster #functional #industrial #roadmap
Trends in functional verification: a 2014 industry study (HDF), p. 6.
DACDAC-2015-GuoDJFM #formal method #perspective #security #validation
Pre-silicon security verification and validation: a formal perspective (XG, RGD, YJ, FF, PM), p. 6.
DACDAC-2015-HerdtLD #simulation #using
Verifying SystemC using stateful symbolic simulation (VH, HML, RD), p. 6.
DACDAC-2015-KleebergerRC #design
Design & verification of automotive SoC firmware (VBK, SR, RC), p. 6.
DACDAC-2015-TodmanSL #configuration management #design #monitoring #runtime
In-circuit temporal monitors for runtime verification of reconfigurable designs (TT, SS, WL), p. 6.
DACDAC-2015-XiaoGWYTW #layout #optimisation #self
Layout optimization and template pattern verification for directed self-assembly (DSA) (ZX, DG, MDFW, HY, MCT, HSPW), p. 6.
DACDAC-2015-ZhengLDGZS #design #security
Design and verification for transportation system security (BZ, WL, PD, LG, QZ, NS), p. 6.
DATEDATE-2015-BergmanBKKMNOPR #experience #industrial
Designer-level verification: an industrial experience story (SB, GB, WK, SK, SM, ZN, AO, VP, WR, GS, VV), pp. 410–411.
DATEDATE-2015-BombieriFPS #abstraction
RTL property abstraction for TLM assertion-based verification (NB, RF, GP, FS), pp. 85–90.
DATEDATE-2015-BurnsSY #modelling #synthesis
GALS synthesis and verification for xMAS models (FPB, DS, AY), pp. 1419–1424.
DATEDATE-2015-KimFPSL #framework #implementation #modelling #platform
Platform-specific timing verification framework in model-based implementation (BK, LF, LTXP, OS, IL), pp. 235–240.
DATEDATE-2015-KonstantinouKM #encryption #functional #privacy
Privacy-preserving functional IP verification utilizing fully homomorphic encryption (CK, AK, MM), pp. 333–338.
DATEDATE-2015-KroeningLMST #bytecode #effectiveness #low level
Effective verification of low-level software with nested interrupts (DK, LL, TM, PS, MT), pp. 229–234.
DATEDATE-2015-KumarLSSH #adaptation
Timing verification for adaptive integrated circuits (RK, BL, YS, US, JH), pp. 1587–1590.
DATEDATE-2015-MadhukarSWKM #abstraction #lazy evaluation #using
Verifying synchronous reactive systems using lazy abstraction (KM, MS, BW, DK, RM), pp. 1571–1574.
DATEDATE-2015-ShonikerCHP #design #process #simulation
Minimizing the number of process corner simulations during design verification (MS, BFC, JH, WP), pp. 289–292.
DATEDATE-2015-SunKPE #algebra #geometry #using
Formal verification of sequential Galois field arithmetic circuits using algebraic geometry (XS, PK, TP, FE), pp. 1623–1628.
LCTESLCTES-2015-LinM #distributed #framework #named #programming #simulation #towards
StarL: Towards a Unified Framework for Programming, Simulating and Verifying Distributed Robotic Systems (YL, SM), p. 10.
LCTESLCTES-2015-ProcterHGBA #design #hardware #implementation #semantics
Semantics Driven Hardware Design, Implementation, and Verification with ReWire (AMP, WLH, IG, MB, GA), p. 10.
PDPPDP-2015-GuthmullerQC #detection #distributed #legacy #similarity
System-Level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications (MG, MQ, GC), pp. 451–458.
PDPPDP-2015-ManciniMMMT #as a service #named
SyLVaaS: System Level Formal Verification as a Service (TM, FM, AM, IM, ET), pp. 476–483.
PPoPPPPoPP-2015-CogumbreiroHMY #concurrent
Dynamic deadlock verification for general barrier synchronisation (TC, RH, FM, NY), pp. 150–160.
ESOPESOP-2015-Penninckx0P #behaviour #composition #source code
Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs (WP, BJ, FP), pp. 158–182.
ESOPESOP-2015-SergeyNB #algorithm #concurrent #specification
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity (IS, AN, AB), pp. 333–358.
FASEFASE-2015-BlomDH
Verification of Loop Parallelisations (SB, SD, MH), pp. 202–217.
FASEFASE-2015-CzechJW #exclamation #what
Just Test What You Cannot Verify! (MC, MCJ, HW), pp. 100–114.
TACASTACAS-2015-AledoE #contest #embedded #framework
FramewORk for Embedded System verification — (Competition Contribution) (PGdA, PSE), pp. 429–431.
TACASTACAS-2015-ArmandoBCCMMM #framework #mobile #named #platform #security #static analysis
SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform (AA, GB, GC, GC, GDM, RM, AM), pp. 225–230.
TACASTACAS-2015-Beyer
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
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation — (Competition Contribution) (YFC, CH, MHT, BYW, FW), pp. 426–428.
TACASTACAS-2015-CiniF #ltl #proving #runtime
An LTL Proof System for Runtime Verification (CC, AF), pp. 581–595.
TACASTACAS-2015-DuggiralaMVP #modelling #named
C2E2: A Verification Tool for Stateflow Models (PSD, SM, MV, MP), pp. 68–82.
TACASTACAS-2015-GurfinkelKN #c #contest #framework #named #source code
SeaHorn: A Framework for Verifying C Programs (Competition Contribution) (AG, TK, JAN), pp. 447–450.
TACASTACAS-2015-HaranCELQR #composition #contest
SMACK+Corral: A Modular Verifier — (Competition Contribution) (AH, MC, ME, AL, SQ, ZR), pp. 451–454.
TACASTACAS-2015-KriouileS #formal method #using
Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip (AK, WS), pp. 708–722.
TACASTACAS-2015-TomascoI0TP15a #concurrent #memory management #source code
Verifying Concurrent Programs by Memory Unwinding (ET, OI, BF, SLT, GP), pp. 551–565.
TACASTACAS-2015-TschannenFNP #functional #named #object-oriented #source code
AutoProof: Auto-Active Functional Verification of Object-Oriented Programs (JT, CAF, MN, NP), pp. 566–580.
CADECADE-2015-DinBH #concurrent #deduction #modelling #named
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS (CCD, RB, RH), pp. 517–526.
CAVCAV-2015-ChatterjeeIP #algorithm #constant #graph #performance
Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs (KC, RIJ, AP), pp. 140–157.
CAVCAV-2015-CookKP #automation #infinity #on the
On Automation of CTL* Verification for Infinite-State Systems (BC, HK, NP), pp. 13–29.
CAVCAV-2015-DasLLL #precise
Angelic Verification: Precise Verification Modulo Unknowns (AD, SKL, AL, YL), pp. 324–342.
CAVCAV-2015-DemyanovaPVZ #benchmark #empirical #metric #tool support
Empirical Software Metrics for Benchmarking of Verification Tools (YD, TP, HV, FZ), pp. 561–579.
CAVCAV-2015-DuggiralaFM0 #challenge
Meeting a Powertrain Verification Challenge (PSD, CF, SM, MV), pp. 536–543.
CAVCAV-2015-GleissenthallKR
Symbolic Polytopes for Quantitative Interpolation and Verification (KvG, BK, AR), pp. 178–194.
CAVCAV-2015-GurfinkelKKN #framework
The SeaHorn Verification Framework (AG, TK, AK, JAN), pp. 343–361.
CAVCAV-2015-LeinoW #fine-grained
Fine-Grained Caching of Verification Results (KRML, VW), pp. 380–397.
CAVCAV-2015-Leslie-HurdCF
Verifying Linearizability of Intel® Software Guard Extensions (RLH, DC, MF), pp. 144–160.
CAVCAV-2015-VijayaraghavanC #composition #deduction #design #hardware #multi
Modular Deductive Verification of Multiprocessor Hardware Designs (MV, AC, A, ND), pp. 109–127.
CAVCAV-2015-ZouFZM #automation #difference #equation #safety
Automatic Verification of Stability and Safety for Delay Differential Equations (LZ, MF, NZ, PNM), pp. 338–355.
ICSTICST-2015-KobashiYWFYOK #design pattern #named #security #testing
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
Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications (HZ, TA, YC), pp. 1–10.
ISSTAISSTA-2015-DimjasevicG #analysis #assurance #generative #runtime #testing
Test-case generation for runtime analysis and vice versa: verification of aircraft separation assurance (MD, DG), pp. 282–292.
TAPTAP-2015-GenestierGP #array #deduction #generative
Sequential Generation of Structured Arrays and Its Deductive Verification (RG, AG, GP), pp. 109–128.
TAPTAP-2015-MoreiraHDMNM #case study #code generation #testing #tool support #using
Verifying Code Generation Tools for the B-Method Using Tests: A Case Study (AMM, CH, DD, ECBdM, JBSN, VdMJ), pp. 76–91.
VMCAIVMCAI-2015-CortesiFPT #mobile #policy #privacy #semantics
Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications (AC, PF, MP, OT), pp. 61–79.
VMCAIVMCAI-2015-DanMVY #abstraction #effectiveness #memory management #modelling
Effective Abstractions for Verification under Relaxed Memory Models (AMD, YM, MTV, EY), pp. 449–466.
VMCAIVMCAI-2015-GjomemoNPVZ #optimisation
From Verification to Optimizations (RG, KSN, PHP, VNV, LDZ), pp. 300–317.
VMCAIVMCAI-2015-KafleG #horn clause #refinement
Tree Automata-Based Refinement with Application to Horn Clause Verification (BK, JPG), pp. 209–226.
QoSAQoSA-2014-JohnsenLPH #dependence #graph #modelling #slicing
Regression verification of AADL models through slicing of system dependence graphs (AJ, KL, PP, KH), pp. 103–112.
QoSAQoSA-2014-Meyer #question #trust
Trust or verify? (BM), pp. 1–2.
DRRDRR-2014-LiPLD #analysis #online
On-line signature verification method by Laplacian spectral analysis and dynamic time warping (CL, LP, CL, XD), p. ?–10.
SANERCSMR-WCRE-2014-MihanceaM #named #security #web
JMODEX: Model extraction for verifying security properties of web applications (PFM, MM), pp. 450–453.
SCAMSCAM-2014-TliliFBDH #scalability #security
Scalable Security Verification of Software at Compile Time (ST, JMF, AB, BD, SH), pp. 115–124.
DLTDLT-2014-YakaryilmazSD #quantum
Debates with Small Transparent Quantum Verifiers (AY, ACCS, HGD), pp. 327–338.
ICALPICALP-v1-2014-Kuncak #recursion
Verifying and Synthesizing Software with Recursive Functions — (Invited Contribution) (VK), pp. 11–25.
LATALATA-2014-GantyR #order
Ordered Counter-Abstraction — Refinable Subword Relations for Parameterized Verification (PG, AR), pp. 396–408.
FMFM-2014-ArenisWDMA #consistency #industrial #standard
The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification (SFA, BW, DD, MM, ASA), pp. 658–672.
FMFM-2014-ArmstrongGS #algebra #concurrent #tool support
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools (AA, VBFG, GS), pp. 78–93.
FMFM-2014-BlomH #concurrent #source code
The VerCors Tool for Verification of Concurrent Programs (SB, MH), pp. 127–131.
FMFM-2014-ChristakisLS #formal method
Formalizing and Verifying a Modern Build Language (MC, KRML, WS), pp. 643–657.
FMFM-2014-DerrickDSTTW #consistency
Quiescent Consistency: Defining and Verifying Relaxed Linearizability (JD, BD, GS, BT, OT, HW), pp. 200–214.
FMFM-2014-GuptaKG #experience
Formally Verifying Graphics FPU — An Intel® Experience (AG, VMAK, RG), pp. 673–687.
FMFM-2014-LeinoM #automation #induction #proving
Co-induction Simply — Automatic Co-inductive Proofs in a Program Verifier (KRML, MM), pp. 382–398.
FMFM-2014-LiuXZS
Formal Verification of Operational Transformation (YL, YX, SJZ, CS), pp. 432–448.
FMFM-2014-MaricS #hardware #memory management #transaction
Verification of a Transactional Memory Manager under Hardware Failures and Restarts (OM, CS), pp. 449–464.
FMFM-2014-ShanWFZZWQC #using
Formal Verification of Lunar Rover Control Software Using UPPAAL (LS, YW, NF, XZ, LZ, LW, LQ, JC), pp. 718–732.
FMFM-2014-ZhaoYZGZC
Formal Verification of a Descent Guidance Control Program of a Lunar Lander (HZ, MY, NZ, BG, LZ, YC), pp. 733–748.
IFMIFM-2014-BrideKP #constraints #specification #theorem proving #using #workflow
Verifying Modal Workflow Specifications Using Constraint Solving (HB, OK, FP), pp. 171–186.
IFMIFM-2014-DerrickSD #architecture
Verifying Linearizability on TSO Architectures (JD, GS, BD), pp. 341–356.
IFMIFM-2014-HentschelKHB #ide #interactive
An Interactive Verification Tool Meets an IDE (MH, SK, RH, RB), pp. 55–70.
IFMIFM-2014-JakobsPWW #hardware
Integrating Software and Hardware Verification (MCJ, MP, HW, TW), pp. 307–322.
IFMIFM-2014-MellerGY #behaviour #uml
Verifying Behavioral UML Systems via CEGAR (YM, OG, KY), pp. 139–154.
SEFMSEFM-2014-ArmstrongGS #higher-order #lightweight #tool support
Lightweight Program Construction and Verification Tools in Isabelle/HOL (AA, VBFG, GS), pp. 5–19.
SEFMSEFM-2014-DiagneMF
A Tool for Verifying Dynamic Properties in B (FD, AM, MF), pp. 290–295.
SEFMSEFM-2014-HauzarK #named #php #web
WeVerca: Web Applications Verification for PHP (DH, JK), pp. 296–301.
SEFMSEFM-2014-LaibinisTGMK #behaviour #formal method #modelling
Formal Modelling and Verification of Cooperative Ant Behaviour in Event-B (LL, ET, ZG, FM, AHK), pp. 363–377.
SEFMSEFM-2014-Leroy #code generation #proving #tool support
Formal Proofs of Code Generation and Verification Tools (XL), pp. 1–4.
SEFMSEFM-2014-ReicherdtG #matlab #modelling #using
Formal Verification of Discrete-Time MATLAB/Simulink Models Using Boogie (RR, SG), pp. 190–204.
SEFMSEFM-2014-RodriguezFHM #erlang #execution #state machine #uml
Execution and Verification of UML State Machines with Erlang (RJR, LÅF, ÁHN, JM), pp. 284–289.
SEFMSEFM-2014-TatsutaC #induction #logic
Completeness of Separation Logic with Inductive Definitions for Program Verification (MT, WNC), pp. 20–34.
SFMSFM-2014-AmighiBDHMZ #concurrent
Verification of Concurrent Systems with VerCors (AA, SB, SD, MH, WM, MZS), pp. 172–216.
ICFPICFP-2014-NguyenTH #contract
Soft contract verification (PCN, STH, DVH), pp. 139–152.
FDGFDG-2014-LogasWMVSSMCOSL #design #game studies
Software verification games: Designing Xylem, The Code of Plants (HL, JW, MM, RV, LS, DGS, JTM, KC, JCO, OS, ZL, HS, MS, DC, SC, CL0).
GT-VMTGT-VMT-2014-WangBL #alloy #graph #model transformation #using
Verification of Graph-based Model Transformations Using Alloy (XW, FB, YL).
ICGTICGT-2014-Delzanno #distributed #model checking #protocol
Parameterized Verification and Model Checking for Distributed Broadcast Protocols (GD), pp. 1–16.
ICGTICGT-2014-PoskittP #graph #higher-order #monad #source code
Verifying Monadic Second-Order Properties of Graph Programs (CMP, DP), pp. 33–48.
ICGTICGT-2014-SelimLCDO #graph #model transformation #specification
Specification and Verification of Graph-Based Model Transformation Properties (GMKS, LL, JRC, JD, BJO), pp. 113–129.
CHICHI-2014-BurgbacherH #gesture #type system
An implicit author verification system for text messages based on gesture typing biometrics (UB, KHH), pp. 2951–2954.
HCIHIMI-DE-2014-TanikawaSKF #design #problem #process #usability
Problems in Usability Improvement Activity by Software Engineers — Consideration through Verification Experiments for Human- Centered Design Process Support Environment (YT, HS, HK, SF), pp. 641–651.
CAiSECAiSE-2014-LaurentBBG #formal method #process
Formalization of fUML: An Application to Process Verification (YL, RB, SB, MPG), pp. 347–363.
ICEISICEIS-v2-2014-AntonioRF #embedded #modelling #process #validation
Verification and Validation Activities for Embedded Systems — A Feasibility Study on a Reading Technique for SysML Models (EAA, RR, SCPFF), pp. 233–240.
CIKMCIKM-2014-YangQ #image #mobile #retrieval #scalability
Spatial Verification for Scalable Mobile Image Retrieval (XY, XQ), pp. 1903–1906.
ICPRICPR-2014-PinheiroRCJS #fuzzy #independence #robust
Type-2 Fuzzy GMMs for Robust Text-Independent Speaker Verification in Noisy Environments (HNBP, TIR, GDCC, IJT, JS), pp. 4531–4536.
ICPRICPR-2014-ZhangWGZZ #analysis #using
Low Computation Face Verification Using Class Center Analysis (XZ, JW, YG, SZ, SZ), pp. 4543–4547.
KRKR-2014-LomuscioM #abstraction #atl #multi #specification
An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications (AL, JM).
SEKESEKE-2014-GuimaraesSALC #alloy #consistency #using
A Method for Verifying the Consistency of Business Rules Using Alloy (DG, EAS, AJA, PL, ALC), pp. 381–386.
SEKESEKE-2014-GuptaAWD #empirical #modelling #using
Evaluating the Use of Model-Based Requirement Verification Method: An Empirical Study (MG, DA, GSW, HD), pp. 397–401.
SEKESEKE-2014-NguyenC #case study #coordination #requirements
Formal Verification of Coordination Systems’ Requirements — A Case Study on the European Train Control System (HNN, ARC), pp. 393–396.
SIGIRSIGIR-2014-DamH #scalability #topic
Large-scale author verification: temporal and topical influences (MvD, CH), pp. 1039–1042.
ECMFAECMFA-2014-LaurentBBG #alloy #framework #process
Alloy4SPV : A Formal Framework for Software Process Verification (YL, RB, SB, MPG), pp. 83–100.
MODELSMoDELS-2014-ChakiE #compilation #distributed #modelling
Model-Driven Verifying Compilation of Synchronous Distributed Applications (SC, JRE), pp. 201–217.
SPLCSPLC-2014-MennickeLSW #automation #feature model #petri net #process #workflow
Automated verification of feature model configuration processes based on workflow Petri nets (SM, ML, JS, TW), pp. 62–71.
SPLCSPLC-2014-SimidchievaO #composition #generative #product line
Generation, composition, and verification of families of human-intensive systems (BIS, LJO), pp. 207–216.
OnwardOnward-2014-VisserWTNVPK #design #implementation
A Language Designer’s Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs (EV, GW, APT, PN, VAV, AP, GK), pp. 95–111.
OOPSLAOOPSLA-2014-WangCC #abstraction #compilation
Compiler verification meets cross-language linking via data abstraction (PW, SC, AC), pp. 675–690.
PEPMPEPM-J-2013-AngelisFPP14
Program verification via iterated specialization (EDA, FF, AP, MP), pp. 149–175.
AdaEuropeAdaEurope-2014-PedroPPP #ada #framework #programming language #runtime #towards
Towards a Runtime Verification Framework for the Ada Programming Language (AdMP, DP, LMP, JSP), pp. 58–73.
HILTHILT-2014-Ball #compilation #correctness #logic #research
Correctness via compilation to logic: a decade of verification at microsoft research (TB), pp. 69–70.
LOPSTRLOPSTR-2014-TahatE #hybrid #protocol #self #synthesis
A Hybrid Method for the Verification and Synthesis of Parameterized Self-Stabilizing Protocols (AT, AE), pp. 201–218.
PEPMPEPM-2014-CosteaSD #named
HIPimm: verifying granular immutability guarantees (AC, AS, CD), pp. 189–194.
PLDIPLDI-2014-BallBGIKSSV #named #network #source code #towards
VeriCon: towards verifying controller programs in software-defined networks (TB, NB, AG, SI, AK, MS, MS, AV), p. 31.
PLDIPLDI-2014-Carbonneaux0RS #bound #c #source code
End-to-end verification of stack-space bounds for C programs (QC, JH, TR, ZS), p. 30.
PLDIPLDI-2014-GreenawayLAK #c
Don’t sweat the small stuff: formal verification of C code without the pain (DG, JL, JA, GK), p. 45.
PLDIPLDI-2014-LogozzoLFB #towards
Verification modulo versions: towards usable verification (FL, SKL, MF, SB), p. 32.
PLDIPLDI-2014-SampsonPMMGC #probability
Expressing and verifying probabilistic assertions (AS, PP, TM, KSM, DG, LC), p. 14.
POPLPOPL-2014-BartheFGSSB #encryption #implementation #probability #relational
Probabilistic relational verification for cryptographic implementations (GB, CF, BG, PYS, NS, SZB), pp. 193–206.
POPLPOPL-2014-BouajjaniEH #consistency #replication
Verifying eventual consistency of optimistic replication systems (AB, CE, JH), pp. 285–296.
POPLPOPL-2014-BurckhardtGYZ #data type #specification
Replicated data types: specification, verification, optimality (SB, AG, HY, MZ), pp. 271–284.
SASSAS-2014-AbdullaHH #exclamation
Block Me If You Can! — Context-Sensitive Parameterized Verification (PAA, FH, LH), pp. 1–17.
SASSAS-2014-ChenHTWW #recursion #source code #using
Verifying Recursive Programs Using Intraprocedural Analyzers (YFC, CH, MHT, BYW, FW), pp. 118–133.
RERE-2014-BadgerTC #analysis #design #named #requirements
VARED: Verification and analysis of requirements and early designs (JMB, DT, CC), pp. 325–326.
RERE-2014-LetychevskyiW #requirements
Symbolic verification of requirements in VRS system (OL, TW), pp. 331–332.
RERE-2014-WittFSH #process #validation
Business Application Modeler: A process model Validation and Verification tool (SW, SF, AS, CH), pp. 333–334.
ASEASE-2014-BasuB #automation #bound #interactive
Automatic verification of interactions in asynchronous systems with unbounded buffers (SB, TB), pp. 743–754.
ASEASE-2014-FelsingGKRU #automation
Automating regression verification (DF, SG, VK, PR, MU), pp. 349–360.
ASEASE-2014-Lopez-FernandezGL #metamodelling #validation
Meta-Model validation and verification with MetaBest (JJLF, EG, JdL), pp. 831–834.
ASEASE-2014-MolotnikovVR #automation #c
Automated domain-specific C verification with mbeddr (ZM, MV, DR), pp. 539–550.
ASEASE-2014-UbayashiALLHK #compilation
Abstraction-aware verifying compiler for yet another MDD (NU, DA, PL, YNL, SH, YK), pp. 557–562.
ASEASE-2014-YangXLCML #adaptation #nondeterminism #self
Verifying self-adaptive applications suffering uncertainty (WY, CX, YL, CC, XM, JL), pp. 199–210.
FSEFSE-2014-Kan #model checking #safety #traceability
Traceability and model checking to support safety requirement verification (SK), pp. 783–786.
FSEFSE-2014-LalQ #using
Powering the static driver verifier using corral (AL, SQ), pp. 202–212.
FSEFSE-2014-Llerena #nondeterminism
Dealing with uncertainty in verification of nondeterministic systems (YRSL), pp. 787–790.
FSEFSE-2014-VakiliD #infinity #modelling #smt #using
Verifying CTL-live properties of infinite state models using an SMT solver (AV, NAD), pp. 213–223.
ICSEICSE-2014-BocicB #induction #invariant #web
Inductive verification of data model invariants for web applications (IB, TB), pp. 620–631.
ICSEICSE-2014-LeP #control flow #graph #interprocedural #multi
Patch verification via multiversion interprocedural control flow graphs (WL, SDP), pp. 1047–1058.
ICSEICSE-2014-MaozRR #component #modelling
Verifying component and connector models against crosscutting structural views (SM, JOR, BR), pp. 95–105.
DACDAC-2014-AdirGHHHHKKLMNPSOTTZ #memory management #transaction
Verification of Transactional Memory in POWER8 (AA, DG, DH, OH, BGH, KH, WK, AK, JML, CM, AN, RRP, MS, BSO, BWT, ET, AZ), p. 6.
DACDAC-2014-ChenWLZAMWH #functional #multi #prototype #standard
A SystemC Virtual Prototyping based Methodology for Multi-Standard SoC Functional Verification (ZC, YW, LL, YZ, AA, JHM, RW, SH), p. 6.
DACDAC-2014-KoestersG
Verification of Non-Mainline Functions in Todays Processor Chips (JK, AG), p. 3.
DACDAC-2014-KrautzPAKPB #automation #float
Automatic Verification of Floating Point Units (UK, VP, AA, SK, SP, TB), p. 6.
DACDAC-2014-LinL #analysis #parallel #reachability
Parallel Hierarchical Reachability Analysis for Analog Verification (HL, PL), p. 6.
DACDAC-2014-PrussKE #abstraction #equivalence #scalability #using
Equivalence Verification of Large Galois Field Arithmetic Circuits using Word-Level Abstraction via Gröbner Bases (TP, PK, FE), p. 6.
DACDAC-2014-Rodriguez-NavasSHNLL #approach #automation #functional #safety #specification
Automated Specification and Verification of Functional Safety in Heavy-Vehicles: the VeriSpec Approach (GRN, CCS, HH, MN, OL, HL), p. 4.
DACDAC-2014-XiaoDTWYWZ #self
Directed Self-Assembly (DSA) Template Pattern Verification (ZX, YD, HT, MDFW, HY, HSPW, HZ), p. 6.
DATEDATE-2014-GuarnieriPSVBFMP #embedded #monitoring
A cross-level verification methodology for digital IPs augmented with embedded timing monitors (VG, MP, AS, SV, NB, FF, EM, MP), pp. 1–6.
DATEDATE-2014-JoostenS #communication #liveness #scalability
Scalable liveness verification for communication fabrics (SJCJ, JS), pp. 1–6.
DATEDATE-2014-KauerSGCA #distributed #embedded #fault tolerance #synthesis
Fault-tolerant control synthesis and verification of distributed embedded systems (MK, DS, DG, SC, AMA), pp. 1–6.
DATEDATE-2014-LeD #design #towards
Towards verifying determinism of SystemC designs (HML, RD), pp. 1–4.
DATEDATE-2014-SubramanyanA #design #security
Formal verification of taint-propagation security properties in a commercial SoC design (PS, DA), pp. 1–2.
DATEDATE-2014-WelpK #invariant #refinement
Property directed invariant refinement for program verification (TW, AK), pp. 1–6.
HPCAHPCA-2014-ZhangBES #design #named #protocol #scalability
PVCoherence: Designing flat coherence protocols for scalable verification (MZ, JDB, JE, DJS), pp. 392–403.
OSDIOSDI-2014-HawblitzelHLNPZZ #automation #security
Ironclad Apps: End-to-End Security via Automated Full-System Verification (CH, JH, JRL, AN, BP, DZ, BZ), pp. 165–181.
PDPPDP-2014-ManciniMMMT #distributed #hardware #manycore #simulation
System Level Formal Verification via Distributed Multi-core Hardware in the Loop Simulation (TM, FM, AM, IM, ET), pp. 734–742.
ESOPESOP-2014-KuwaharaTU0 #automation #functional #higher-order #source code #termination
Automatic Termination Verification for Higher-Order Functional Programs (TK, TT, HU, NK), pp. 392–411.
ESOPESOP-2014-PercontiA #compilation #multi #semantics #using
Verifying an Open Compiler Using Multi-language Semantics (JTP, AA), pp. 128–148.
FASEFASE-2014-MasciZJCT #user interface #using
Formal Verification of Medical Device User Interfaces Using PVS (PM, YZ, PLJ, PC, HWT), pp. 200–214.
FASEFASE-2014-Zaharieva-StojanovskiH #concurrent #invariant #source code
Verifying Class Invariants in Concurrent Programs (MZS, MH), pp. 230–245.
TACASTACAS-2014-AngelisFPP #named #source code
VeriMAP: A Tool for Verifying Programs through Transformations (EDA, FF, AP, MP), pp. 568–574.
TACASTACAS-2014-Ardeshir-LarijaniGN #concurrent #equivalence #protocol #quantum
Verification of Concurrent Quantum Protocols by Equivalence Checking (EAL, SJG, RN), pp. 500–514.
TACASTACAS-2014-Beyer #contest #summary
Status Report on Software Verification — (Competition Summary SV-COMP 2014) (DB0), pp. 373–388.
TACASTACAS-2014-EldibWS #smt
SMT-Based Verification of Software Countermeasures against Side-Channel Attacks (HE, CW, PS), pp. 62–77.
TACASTACAS-2014-GurfinkelB #contest #named
FrankenBit: Bit-Precise Verification with Many Bits — (Competition Contribution) (AG, AB), pp. 408–411.
TACASTACAS-2014-HartmannsH #ide #modelling #tool support
The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification (AH, HH), pp. 593–598.
TACASTACAS-2014-PiskacWZ #named #specification
GRASShopper — Complete Heap Verification with Mixed Specifications (RP, TW, DZ), pp. 124–139.
TACASTACAS-2014-Siirtola #bound #composition #multi #named
Bounds2: A Tool for Compositional Multi-parametrised Verification (AS), pp. 599–604.
WRLAWRLA-2014-BartolettiMSZ #maude #modelling
Modelling and Verifying Contract-Oriented Systems in Maude (MB, MM, AS, RZ), pp. 130–146.
CAVCAV-2014-AbdullaACHRRS #constraints #string
String Constraints for Verification (PAA, MFA, YFC, LH, AR, PR, JS), pp. 150–166.
CAVCAV-2014-BardsleyBCCDDKLQ #gpu #kernel
Engineering a Static Verification Tool for GPU Kernels (EB, AB, NC, PC, PD, AFD, JK, DL, SQ), pp. 226–242.
CAVCAV-2014-BeyerDW
Software Verification in the Google App-Engine Cloud (DB, GD, PW), pp. 327–333.
CAVCAV-2014-BinghamL #bound #fault #simulation #using
Verifying Relative Error Bounds Using Symbolic Simulation (JB, JLH), pp. 277–292.
CAVCAV-2014-CermakLMM #logic #model checking #named #specification
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PC, AL, FM, AM), pp. 525–532.
CAVCAV-2014-CimattiGMT #hybrid #ltl
Verifying LTL Properties of Hybrid Systems with K-Liveness (AC, AG, SM, ST), pp. 424–440.
CAVCAV-2014-FerraraMNP #data access #named #policy
Vac — Verifier of Administrative Role-Based Access Control Policies (ALF, PM, TLN, GP), pp. 184–191.
CAVCAV-2014-HuangFMMK #automaton #hybrid #invariant #network
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells (ZH, CF, AM, SM, MZK), pp. 373–390.
CAVCAV-2014-LeeS #abstraction #approximate #bound #reachability #scalability
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (SL, KAS), pp. 849–865.
CAVCAV-2014-LesaniMP #automation #concurrent #data type
Automatic Atomicity Verification for Clients of Concurrent Data Structures (ML, TDM, JP), pp. 550–567.
CAVCAV-2014-RakamaricE #implementation #named
SMACK: Decoupling Source Language Details from Verifier Implementations (ZR, ME), pp. 106–113.
CAVCAV-2014-SanchezS #concurrent #data type #named
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (AS, CS), pp. 620–627.
IJCARIJCAR-2014-Zhang #encoding
QBF Encoding of Temporal Properties and QBF-Based Verification (WZ), pp. 224–239.
ISSTAISSTA-2014-ShachamYGABSV #independence
Verifying atomicity via data independence (OS, EY, GGG, AA, NGB, MS, MTV), pp. 26–36.
LICSLICS-CSL-2014-LiangFS #composition #concurrent #refinement #source code
Compositional verification of termination-preserving refinement of concurrent programs (HL, XF, ZS), p. 10.
SMTSMT-2014-Melquiond #algorithm #automation #float
Automating the Verification of Floating-Point Algorithms (GM), p. 63.
TAPTAP-2014-DiepenbeckKSD #behaviour #development #testing
Behaviour Driven Development for Tests and Verification (MD, UK, MS, RD), pp. 61–77.
TAPTAP-2014-HilkenNGW #behaviour #comparison #modelling #ocl #uml
Filmstripping and Unrolling: A Comparison of Verification Approaches for UML and OCL Behavioral Models (FH, PN, MG, RW), pp. 99–116.
TAPTAP-2014-KampmannGZ #bound #execution #named #performance
JTACO: Test Execution for Faster Bounded Verification (AK, JPG, AZ), pp. 134–141.
TAPTAP-2014-KanigCCGMR
Explicit Assumptions — A Prenup for Marrying Static and Dynamic Program Verification (JK, RC, CC, JG, YM, ER), pp. 142–157.
TAPTAP-2014-KosmatovLA #case study #proving #testing
A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing (NK, ML, CA), pp. 158–164.
TAPTAP-2014-PetiotKGJ #deduction #generative #how #specification #testing
How Test Generation Helps Software Specification and Deductive Verification in Frama-C (GP, NK, AG, JJ), pp. 204–211.
VMCAIVMCAI-2014-AngelisFPP #array #source code
Verifying Array Programs by Transforming Verification Conditions (EDA, FF, AP, MP), pp. 182–202.
VMCAIVMCAI-2014-DragoiHVWZ #algorithm #framework
A Logic-Based Framework for Verifying Consensus Algorithms (CD, TAH, HV, JW, DZ), pp. 161–181.
VMCAIVMCAI-2014-JezequelE #algorithm #distributed #message passing #protocol
Message-Passing Algorithms for the Verification of Distributed Protocols (LJ, JE), pp. 222–241.
CBSECBSE-2013-BarnatBCP #component #named
DCCL: verification of component systems with ensembles (JB, NB, IC, ZP), pp. 43–52.
CBSECBSE-2013-JohnsonCK #component #framework #incremental
An incremental verification framework for component-based software systems (KJ, RC, SK), pp. 33–42.
DRRDRR-2013-RicquebourgCG #evaluation #recognition #robust #word
Evaluation of lexicon size variations on a verification and rejection system based on SVM, for accurate and robust recognition of handwritten words (YR, BC, LG).
DRRDRR-2013-SrihariKTB #using
Combining evidence using likelihood ratios in writer verification (SNS, DK, YT, GRB).
ICDARICDAR-2013-HuC #classification #pseudo #using
Offline Signature Verification Using Real Adaboost Classifier Combination of Pseudo-dynamic Features (JH, YC), pp. 1345–1349.
ICDARICDAR-2013-JainD #detection #documentation #image #named
VisualDiff: Document Image Verification and Change Detection (RJ, DSD), pp. 40–44.
ICDARICDAR-2013-KamihiraOWK
Improvement of Japanese Signature Verification by Segmentation-Verification (YK, WO, TW, FK), pp. 379–382.
ICDARICDAR-2013-KhanKS #identification #problem #question
Can Signature Biometrics Address Both Identification and Verification Problems? (SHK, ZK, FS), pp. 981–985.
ICDARICDAR-2013-KhayyatLS #classification #word
Verification of Hierarchical Classifier Results for Handwritten Arabic Word Spotting (MK, LL, CYS), pp. 572–576.
ICDARICDAR-2013-LiPXW #analysis #consistency #online #order
A Stroke Order Verification Method for On-Line Handwritten Chinese Characters Based on Tempo-spatial Consistency Analysis (RL, LP, EX, NW), pp. 999–1003.
ICDARICDAR-2013-MalikALD #forensics #realtime
FREAK for Real Time Forensic Signature Verification (MIM, SA, ML, AD), pp. 971–975.
ICDARICDAR-2013-MalikLAOBF #contest #identification
ICDAR 2013 Competitions on Signature Verification and Writer Identification for On- and Offline Skilled Forgeries (SigWiComp 2013) (MIM, ML, LA, WO, MB, BF), pp. 1477–1483.
ICDARICDAR-2013-MalikLD #automation #comparison #forensics
Part-Based Automatic System in Comparison to Human Experts for Forensic Signature Verification (MIM, ML, AD), pp. 872–876.
PODSPODS-2013-AbouziedAPHS #learning #quantifier #query
Learning and verifying quantified boolean queries by example (AA, DA, CHP, JMH, AS), pp. 49–60.
PODSPODS-2013-BojanczykST
Verification of database-driven systems via amalgamation (MB, LS, ST), pp. 63–74.
PODSPODS-2013-HaririCGDM #relational
Verification of relational data-centric dynamic systems with external services (BBH, DC, GDG, AD, MM), pp. 163–174.
ICALPICALP-v2-2013-DemriDS #complexity #on the
On the Complexity of Verifying Regular Properties on Flat Counter Systems, (SD, AKD, AS), pp. 162–173.
LATALATA-2013-DelzannoT #complexity #decidability #network
Decidability and Complexity Results for Verification of Asynchronous Broadcast Networks (GD, RT), pp. 238–249.
LATALATA-2013-Etessami #algorithm #infinity #probability #recursion
Algorithms for Analyzing and Verifying Infinite-State Recursive Probabilistic Systems (KE), p. 12.
IFMIFM-2013-GavaFG #algorithm #deduction
Deductive Verification of State-Space Algorithms (FG, JF, MG), pp. 124–138.
IFMIFM-2013-IshiiMN #automaton #calculus #hybrid #induction
Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus (DI, GM, SN), pp. 139–153.
IFMIFM-2013-MeryP #formal method #modelling #protocol
Formal Modelling and Verification of Population Protocols (DM, MP), pp. 208–222.
IFMIFM-2013-MilloRKN #composition #product line
Compositional Verification of Software Product Lines (JVM, SR, SNK, GKN), pp. 109–123.
IFMIFM-2013-MoranHS #automation
Automated Anonymity Verification of the ThreeBallot Voting System (MM, JH, SS), pp. 94–108.
IFMIFM-2013-SavaryFL #bytecode #detection #modelling #testing #using
Detecting Vulnerabilities in Java-Card Bytecode Verifiers Using Model-Based Testing (AS, MF, JLL), pp. 223–237.
IFMIFM-2013-VekrisLDM #specification #using
Verification of EB3 Specifications Using CADP (DV, FL, CD, RM), pp. 61–76.
SEFMSEFM-2013-BoerGW #runtime
Run-Time Verification of Coboxes (FSdB, SdG, PYHW), pp. 259–273.
SEFMSEFM-2013-GesellMS
Lifting Verification Results for Preemption Statements (MG, AM, KS), pp. 91–105.
SEFMSEFM-2013-Klimek #logic #modelling #requirements #specification
From Extraction of Logical Specifications to Deduction-Based Formal Verification of Requirements Models (RK), pp. 61–75.
SEFMSEFM-2013-PerceboisST #graph transformation #invariant #transitive
Rule-Level Verification of Graph Transformations for Invariants Based on Edges’ Transitive Closure (CP, MS, HNT), pp. 106–121.
SEFMSEFM-2013-SuryadevaraSMP #behaviour #using
Verifying MARTE/CCSL Mode Behaviors Using UPPAAL (JS, CCS, FM, PP), pp. 1–15.
ICFPICFP-2013-BroadbentCHS #approach #higher-order #named
C-SHORe: a collapsible approach to higher-order verification (CHB, AC, MH, OS), pp. 13–24.
ICFPICFP-2013-Chlipala #generative #hoare #logic #metaprogramming
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier (AC), pp. 391–402.
ICFPICFP-2013-LorenzenE #automation #composition
Modular and automated type-soundness verification for language extensions (FL, SE), pp. 331–342.
IFLIFL-2013-GijzelN #framework #implementation #modelling #towards
Towards a framework for the implementation and verification of translations between argumentation models (BvG, HN), p. 93.
GCMGCM-J-2012-PoskittP #correctness #graph #source code
Verifying Total Correctness of Graph Programs (CMP, DP).
CHICHI-2013-Egelman #exclamation #facebook #privacy #trade-off
My profile is my password, verify me!: the privacy/convenience tradeoff of facebook connect (SE), pp. 2369–2378.
HCIDHM-HB-2013-XieKD #modelling
Anatomy-Based Variational Modeling of Digital Hand and Its Verification (YX, SK, HD), pp. 384–392.
HCIHIMI-HSM-2013-KimKL #design #standard
Designing and Verifying Application Schema by Applying Standard Element for Managing Ocean Observation Data (STK, LKK, TYL), pp. 110–115.
EDOCEDOC-2013-TranZ #analysis #approach #architecture
Event Actors Based Approach for Supporting Analysis and Verification of Event-Driven Architectures (HT, UZ), pp. 217–226.
KDIRKDIR-KMIS-2013-AlwazaePK #classification
Verifying the Usefulness of a Classification System of Best Practices (MMSA, EP, HK), pp. 405–412.
MODELSMoDELS-2013-PiresPWD #behaviour #embedded #source code
Behavioural Verification in Embedded Software, from Model to Source Code (AFP, TP, VW, SD), pp. 320–335.
MODELSMoDELS-2013-SelimBCDW #automation #industrial #model transformation
Automated Verification of Model Transformations in the Automotive Industry (GMKS, FB, JRC, JD, SW), pp. 690–706.
MODELSMoDELS-2013-ZalilaCP #approach #domain-specific language #integration
Formal Verification Integration Approach for DSML (FZ, XC, MP), pp. 336–351.
ECOOPECOOP-2013-HeuleKMS #abstraction #generative #logic
Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions (SH, ITK, PM, AJS), pp. 451–476.
OOPSLAOOPSLA-2013-CarbinMR #hardware #reliability #source code
Verifying quantitative reliability for programs that execute on unreliable hardware (MC, SM, MCR), pp. 33–52.
HILTHILT-2013-Alagic #automation #interactive
Automatic versus interactive program verification (SA), pp. 87–88.
HILTHILT-2013-EfstathopoulosH #optimisation
Optimizing verification effort with SPARK 2014 (PE, AH), pp. 19–20.
HILTHILT-2013-Logozzo #contract #specification
Practical specification and verification with code contracts (FL), pp. 7–8.
HILTHILT-2013-MurugesanWRH #composition
Compositional verification of a medical device system (AM, MWW, SR, MPEH), pp. 51–64.
LOPSTRLOPSTR-2013-Vidal #erlang #term rewriting #towards
Towards Erlang Verification by Term Rewriting (GV), pp. 109–126.
PEPMPEPM-2013-AngelisFPP #source code
Verifying programs via iterated specialization (EDA, FF, AP, MP), pp. 43–52.
PLDIPLDI-2013-LiangF #composition
Modular verification of linearizability with non-fixed linearization points (HL, XF), pp. 459–470.
PLDIPLDI-2013-SwamyWSCL #higher-order #monad #source code
Verifying higher-order programs with the dijkstra monad (NS, JW, CS, JC, BL), pp. 387–398.
PLDIPLDI-2013-ZhaoNMZ #optimisation
Formal verification of SSA-based optimizations for LLVM (JZ, SN, MMKM, SZ), pp. 175–186.
POPLPOPL-2013-UnnoTK #automation #functional #higher-order #source code
Automating relatively complete verification of higher-order functional programs (HU, TT, NK), pp. 75–86.
SASSAS-2013-0001GHAN #concept #geometry #learning
Verification as Learning Geometric Concepts (RS, SG, BH, AA, AVN), pp. 388–411.
SASSAS-2013-BlazyLMP #abstract interpretation #analysis #c
Formal Verification of a C Value Analysis Based on Abstract Interpretation (SB, VL, AM, DP), pp. 324–344.
SASSAS-2013-BrainDGHK #float #source code
Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL (MB, VD, AG, LH, DK), pp. 412–432.
SASSAS-2013-DOsualdoKO #automation #concurrent
Automatic Verification of Erlang-Style Concurrency (ED, JK, CHLO), pp. 454–476.
SASSAS-2013-DudkaPV #low level
Byte-Precise Verification of Low-Level List Manipulation (KD, PP, TV), pp. 215–237.
SASSAS-2013-MajumdarMW #message passing #source code
Static Provenance Verification for Message Passing Programs (RM, RM, ZW), pp. 366–387.
RERE-2013-GhezziMSS #on the #requirements
On requirements verification for model refinements (CG, CM, AMS, PS), pp. 62–71.
ASEASE-2013-0002IP #c #concurrent #named #preprocessor #tool support
CSeq: A concurrency pre-processor for sequential C verification tools (BF, OI, GP), pp. 710–713.
ASEASE-2013-CalinescuJR #self
Developing self-verifying service-based systems (RC, KJ, YR), pp. 734–737.
ASEASE-2013-DhunganaTWW #automation #interactive #rule-based
Automated verification of interactive rule-based configuration systems (DD, CHT, CW, PW), pp. 551–561.
ASEASE-2013-Frank #automation #challenge #validation
The challenges of verification and validation of automated planning systems (JF), p. 2.
ASEASE-2013-MaezawaWTH #ajax #automation #interactive #invariant
Automated verification of pattern-based interaction invariants in Ajax applications (YM, HW, YT, SH), pp. 158–168.
ASEASE-2013-MeredithR #parametricity #performance #runtime #string
Efficient parametric runtime verification with deterministic string rewriting (POM, GR), pp. 70–80.
ESEC-FSEESEC-FSE-2013-BeyerLNSW #performance #precise #reuse
Precision reuse for efficient regression verification (DB, SL, EN, AS, PW), pp. 389–399.
ESEC-FSEESEC-FSE-2013-NavabpourJWBMBF #c #named #runtime #source code
RiTHM: a tool for enabling time-triggered runtime verification for C programs (SN, YJ, CWWW, SB, RM, BB, SF), pp. 603–606.
ESEC-FSEESEC-FSE-2013-ZervoudakisREF #model checking
Cascading verification: an integrated method for domain-specific model checking (FZ, DSR, SGE, AF), pp. 400–410.
ICSEICSE-2013-ApelRWGB #case study #product line
Strategies for product-line verification: case studies and experiments (SA, AvR, PW, AG, DB), pp. 482–491.
ICSEICSE-2013-BohmeOR
Partition-based regression verification (MB, BCdSO, AR), pp. 302–311.
ICSEICSE-2013-HatcliffRCB #execution #framework #symbolic computation
Explicating symbolic execution (xSymExe): an evidence-based verification framework (JH, R, PC, JB), pp. 222–231.
SACSAC-2013-CogniniFPPR #collaboration #modelling #named #process
HawkEye: a tool for collaborative business process modelling and verification (RC, DF, AP, AP, BR), pp. 785–786.
SACSAC-2013-MartinaP #induction #multi #protocol #security #using
Verifying multicast-based security protocols using the inductive method (JEM, LCP), pp. 1824–1829.
SLESLE-2013-PearceG #framework #named #platform #research
Whiley: A Platform for Research in Software Verification (DJP, LG), pp. 238–248.
ASPLOSASPLOS-2013-CuiHWY #execution #symbolic computation #using
Verifying systems rules using rule-directed symbolic execution (HC, GH, JW, JY), pp. 329–342.
ASPLOSASPLOS-2013-MaiPXKM #invariant #security
Verifying security invariants in ExpressOS (HM, EP, HX, STK, PM), pp. 293–304.
CASECASE-2013-MohajeraniMF #automaton #composition #finite #using
Compositional nonblocking verification for extended finite-state automata using partial unfolding (SM, RM, MF), pp. 930–935.
DACDAC-2013-ChenWBA #random #reuse #simulation
Simulation knowledge extraction and reuse in constrained random processor verification (WC, LCW, JB, MSA), p. 6.
DACDAC-2013-Feng #grid #power management #scalability
Scalable vectorless power grid current integrity verification (ZF), p. 8.
DACDAC-2013-GoswamiLKSMCR #development #modelling
Model-based development and verification of control software for electric vehicles (DG, ML, MK, SS, AM, SC, SR), p. 9.
DACDAC-2013-LeGHD #simulation #using
Verifying SystemC using an intermediate verification language and symbolic simulation (HML, DG, VH, RD), p. 6.
DACDAC-2013-LinLM #analysis #hybrid #kernel #reachability
Verification of digitally-intensive analog circuits via kernel ridge regression and hybrid reachability analysis (HL, PL, CJM), p. 6.
DACDAC-2013-WuH #constraints #framework #multi #random #robust #set #theorem proving
A robust constraint solving framework for multiple constraint sets in constrained random verification (BHW, CY(H), p. 7.
DACDAC-2013-XiongW #abstraction #constraints #grid #power management
Constraint abstraction for vectorless power grid verification (XX, JW), p. 6.
DACDAC-2013-ZhangYWSX #hardware #named #trust
VeriTrust: verification for hardware trust (JZ, FY, LW, ZS, QX), p. 8.
DATEDATE-2013-AbdullaDRSZ #hybrid #liveness #memory management #safety #transaction
Verifying safety and liveness for the FlexTM hybrid transactional memory (PAA, SD, AR, AS, YZ), pp. 785–790.
DATEDATE-2013-AhmadyanKV #algorithm #incremental #runtime #using
Runtime verification of nonlinear analog circuits using incremental time-augmented RRT algorithm (SNA, JAK, SV), pp. 21–26.
DATEDATE-2013-FreitasRS #concurrent #consistency #memory management #on the fly
On-the-fly verification of memory consistency with concurrent relaxed scoreboards (LSF, EAR, LCVdS), pp. 631–636.
DATEDATE-2013-MillerB #parametricity #satisfiability
Formal verification of analog circuit parameters across variation utilizing SAT (MM, FB), pp. 1442–1447.
DATEDATE-2013-SeiterWSD #ocl #specification #uml
Determining relevant model elements for the verification of UML/OCL specifications (JS, RW, MS, RD), pp. 1189–1192.
DATEDATE-2013-WilleGSKD #modelling #towards
Towards a generic verification methodology for system models (RW, MG, MS, MK, RD), pp. 1193–1196.
HPCAHPCA-2013-BeuPHC #performance
High-speed formal verification of heterogeneous coherence hierarchies (JGB, JAP, ERH, TMC), pp. 566–577.
PDPPDP-2013-DrumlMSWGBH #behaviour #design #functional #performance
Emulation-Based Test and Verification of a Design’s Functional, Performance, Power, and Supply Voltage Behavior (ND, MM, CS, RW, AG, HB, JH), pp. 328–335.
PLOSPLOS-2013-KellerMAOCRKH #exclamation #file system
File systems deserve verification too! (GK, TCM, SA, LO, ZC, LR, GK, GH), p. 7.
PPoPPPPoPP-2013-BartheCKGM #relational #synthesis
From relational verification to SIMD loop synthesis (GB, JMC, SG, CK, MM), pp. 123–134.
SOSPSOSP-2013-BraunFRSBW
Verifying computations with state (BB, AJF, ZR, STVS, AJB, MW), pp. 341–357.
ESOPESOP-2013-AlglaveKNT #memory management #program transformation
Software Verification for Weak Memory via Program Transformation (JA, DK, VN, MT), pp. 512–532.
ESOPESOP-2013-BouajjaniEEH #concurrent #source code #specification
Verifying Concurrent Programs against Sequential Specifications (AB, ME, CE, JH), pp. 290–309.
ESOPESOP-2013-CollingbourneDKQ #analysis #gpu #kernel #semantics
Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels (PC, AFD, JK, SQ), pp. 270–289.
ESOPESOP-2013-GotsmanRY #algorithm #concurrent #memory management
Verifying Concurrent Memory Reclamation Algorithms with Grace (AG, NR, HY), pp. 249–269.
ESOPESOP-2013-KassiosK
A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness (ITK, EK), pp. 149–168.
FASEFASE-2013-GudemannPSD #framework #named
VerChor: A Framework for Verifying Choreographies (MG, PP, GS, AD), pp. 226–230.
FASEFASE-2013-NordioCF #javascript #named
Javanni: A Verifier for JavaScript (MN, CC, CAF), pp. 231–234.
FoSSaCSFoSSaCS-2013-MioS #composition #concurrent #probability #process #proving
A Proof System for Compositional Verification of Probabilistic Concurrent Processes (MM, AS), pp. 161–176.
TACASTACAS-2013-AbdullaHHJR #concurrent #data type #specification
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures (PAA, FH, LH, BJ, AR), pp. 324–338.
TACASTACAS-2013-AlbarghouthiGLCC #abstract interpretation #contest #named
UFO: Verification with Interpolants and Abstract Interpretation — (Competition Contribution) (AA, AG, YL, SC, MC), pp. 637–640.
TACASTACAS-2013-Beyer #contest #summary
Second Competition on Software Verification — (Summary of SV-COMP 2013) (DB0), pp. 594–609.
TACASTACAS-2013-DudkaMPV #contest #low level #named
Predator: A Tool for Verification of Low-Level List Manipulation — (Competition Contribution) (KD, PM, PP, TV), pp. 627–629.
TACASTACAS-2013-GrigoreDPT #automaton #runtime
Runtime Verification Based on Register Automata (RG, DD, RLP, NT), pp. 260–276.
TACASTACAS-2013-PopeeaR #concurrent #contest #multi #named #source code #thread
Threader: A Verifier for Multi-threaded Programs — (Competition Contribution) (CP, AR), pp. 633–636.
CADECADE-2013-HahnleSB #reuse
Reuse in Software Verification by Abstract Method Calls (RH, IS, RB), pp. 300–314.
CADECADE-2013-HeuleHW
Verifying Refutations with Extended Resolution (MH, WAHJ, NW), pp. 345–359.
CADECADE-2013-Sofronie-Stokkermans #generative #hybrid #parametricity #reasoning
Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems (VSS), pp. 360–376.
CAVCAV-2013-BraibantC #hardware #synthesis
Formal Verification of Hardware Synthesis (TB, AC), pp. 213–228.
CAVCAV-2013-EsparzaGM
Parameterized Verification of Asynchronous Shared-Memory Systems (JE, PG, RM), pp. 124–140.
CAVCAV-2013-KongHSHG #generative #hybrid #safety
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems (HK, FH, XS, WNNH, MG), pp. 242–257.
CAVCAV-2013-ManciniMMMMT #model checking #simulation
System Level Formal Verification via Model Checking Driven Simulation (TM, FM, AM, IM, FM, ET), pp. 296–312.
CAVCAV-2013-PuggelliLSS #nondeterminism #polynomial
Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties (AP, WL, ALSV, SAS), pp. 527–542.
CAVCAV-2013-RummerHK
Disjunctive Interpolants for Horn-Clause Verification (PR, HH, VK), pp. 347–363.
ICLPICLP-J-2013-GiordanoMSD #constraints #process #programming #set
Business process verification with constraint temporal answer set programming (LG, AM, MS, DTD), pp. 641–655.
ICSTICST-2013-KangKHKNSC #formal method #modelling
Formal Modeling and Verification of SDN-OpenFlow (MK, EYEK, DYH, BJK, KHN, MKS, JYC), pp. 481–482.
ISSTAISSTA-2013-Thum #contract #feature model #product line
Product-line verification with feature-oriented contracts (TT), pp. 374–377.
TAPTAP-2013-ArthoBS #modelling #testing
Model-Based Testing for Verification Back-Ends (CA, AB, MS), pp. 39–55.
TAPTAP-2013-BeckertB0 #metric #testing
A Metric for Testing Program Verification Systems (BB, TB, MW), pp. 56–75.
DRRDRR-2012-CoetzerSS #collaboration #human-computer #performance
Efficient cost-sensitive human-machine collaboration for offline signature verification (JC, JPS, RS).
DRRDRR-2012-NagyT #named #performance
VeriClick: an efficient tool for table format verification (GN, MT).
VLDBVLDB-2012-GoodrichNOPTTL #authentication #crawling #performance #web
Efficient Verification of Web-Content Searching Through Authenticated Web Crawlers (MTG, DN, OO, CP, RT, NT, CVL), pp. 920–931.
CSEETCSEET-2012-Virseda #algebra #data type #implementation #specification #testing
A Software Testing Tool for the Verification of Abstract Data Type Implementations from Formal Algebraic Specifications (RdVV), pp. 100–104.
CSMRCSMR-2012-CastrejonLV #architecture #maintenance #named #web
Web2MexADL: Discovery and Maintainability Verification of Software Systems Architecture (JCC, RL, GVS), pp. 531–534.
MSRMSR-2012-SouzaC #debugging #ide #open source
Characterizing verification of bug fixes in two open source IDEs (RS, CC), pp. 70–73.
SCAMSCAM-2012-Vidal #execution #symbolic computation #termination
Closed Symbolic Execution for Verifying Program Termination (GV), pp. 34–43.
FMFM-2012-ChristakisMW #collaboration #testing
Collaborative Verification and Testing with Explicit Assumptions (MC, PM, VW), pp. 132–146.
FMFM-2012-HojjatKGIKR #tool support
A Verification Toolkit for Numerical Transition Systems — Tool Paper (HH, FK, FG, RI, VK, PR), pp. 247–251.
FMFM-2012-JohnsonGMDE #case study #hybrid
Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems (TTJ, JG, SM, RD, RSE), pp. 252–266.
FMFM-2012-LinLSDA #automation #composition
Automatic Compositional Verification of Timed Systems (SWL, YL, JS, JSD, ÉA), pp. 272–276.
IFMIFM-2012-BlackmoreHBER #automation #generative #simulation
Analysing and Closing Simulation Coverage by Automatic Generation and Verification of Formal Properties from Coverage Reports (TB, DH, PB, KE, NR), pp. 84–98.
IFMIFM-2012-CalderS #algebra #case study #network #process #runtime
Process Algebra for Event-Driven Runtime Verification: A Case Study of Wireless Network Management (MC, MS), pp. 21–23.
IFMIFM-2012-NgoTGGB #compilation #equation
Formal Verification of Compiler Transformations on Polychronous Equations (VCN, JPT, TG, PLG, LB), pp. 113–127.
IFMIFM-2012-RochaCMS #execution #interactive
A Formal Interactive Verification Environment for the Plan Execution Interchange Language (CR, HC, CAM, RS), pp. 343–357.
IFMIFM-2012-TarasyukTL #formal method #modelling #probability
Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B (AT, ET, LL), pp. 237–252.
RTARTA-2012-Lisitsa #automaton #finite #modelling #safety
Finite Models vs Tree Automata in Safety Verification (AL), pp. 225–239.
SEFMSEFM-2012-BicknellRBCS #approach #using
A Practical Approach for Closed Systems Formal Verification Using Event-B (BB, JR, MJB, JC, CFS), pp. 323–332.
SEFMSEFM-2012-ColomboFMP #bound #configuration management #monitoring #named #resource management #runtime
polyLarva: Runtime Verification with Configurable Resource-Aware Monitoring Boundaries (CC, AF, RM, GJP), pp. 218–232.
SEFMSEFM-2012-PaulSS #assembly #automation
Completing the Automated Verification of a Small Hypervisor — Assembler Code Verification (WJP, SS, AS), pp. 188–202.
SEFMSEFM-2012-ZhangKJ #composition
Verification of Aspectual Composition in Feature-Modeling (QZ, RK, JJ), pp. 109–125.
SEFMSEFM-2012-ZhuXMQQ #approach #concurrent #source code
The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs (HZ, QX, CM, SQ, ZQ), pp. 172–187.
FLOPSFLOPS-2012-Terauchi #automation #functional #higher-order #source code
Automated Verification of Higher-Order Functional Programs (TT), p. 2.
ICFPICFP-2012-Huffman #monad
Formal verification of monad transformers (BH), pp. 15–16.
ICGTICGT-2012-GieseL #automation #behaviour #invariant #model transformation #towards
Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking (HG, LL), pp. 249–263.
ICGTICGT-2012-Poskitt #graph #source code
Verification of Graph Programs (CMP), pp. 420–422.
ICGTICGT-2012-Vandin #specification
Specification and Verification of Modal Properties for Structured Systems (AV), pp. 423–425.
CAiSECAiSE-2012-Razo-ZapataLGA #fuzzy #network
Fuzzy Verification of Service Value Networks (ISRZ, PDL, JG, HA), pp. 95–110.
ICEISICEIS-v2-2012-CapelM #approach #automation #composition #correctness #model checking #safety
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-KennardBS #2d #approach #detection #geometry #using
Offline signature verification and forgery detection using a 2-D geometric warping approach (DJK, WAB, TWS), pp. 3733–3736.
ICPRICPR-2012-MaoYLZ #classification #invariant
Age-invariant face verification based on Local Classifier Ensemble (XJM, YBY, NL, YZ), pp. 2408–2411.
ICPRICPR-2012-NgC #using
Face verification using temporal affective cues (ESN, AYSC), pp. 1249–1252.
ICPRICPR-2012-StrucZP #normalisation #parametricity
Non-parametric score normalization for biometric verification systems (VS, JZG, NP), pp. 2395–2399.
ICPRICPR-2012-XiaSF #towards #using #visual notation
Toward kinship verification using visual attributes (SX, MS, YF), pp. 549–552.
KRKR-2012-BelardinelliLP #abstraction
An Abstraction Technique for the Verification of Artifact-Centric Systems (FB, AL, FP).
KRKR-2012-GiacomoLP #bound #calculus #decidability
Bounded Situation Calculus Action Theories and Decidable Verification (GDG, YL, FP).
KRKR-2012-HaufeT #automation #game studies
Automated Verification of Epistemic Properties for General Game Playing (SH, MT).
SEKESEKE-2012-BouchenebB #parametricity #workflow
Parametric Verification of TimeWorkflow Nets (HB, KB), pp. 375–380.
SEKESEKE-2012-CuiWLBZL #aspect-oriented #diagrams #petri net #process
Verifying Aspect-Oriented Activity Diagrams Against Crosscutting Properties with Petri Net Analyzer (ZC, LW, XL, LB, JZ, XL), pp. 369–374.
SEKESEKE-2012-DuttaUA #analysis #approach #automation #semantics
Requirement Analysis and Automated Verification: A Semantic Approach (AD, PDU, SA), pp. 51–54.
SEKESEKE-2012-LiLCZJZ #adaptation #continuation #self
A HybridUML and QdL Based Verification Method for CPS Self-Adaptability (JL, BL, QC, MZ, SJ, XZ), pp. 239–242.
SEKESEKE-2012-ShenHTGZ #feature model #logic #modelling
Feature modeling and Verification based on Description Logics (GS, ZH, CT, QG, WZ), pp. 422–425.
SEKESEKE-2012-ZhaiLZLCJ #algebra #cyber-physical #logic
Verification of Cyber-Physical Systems Based on Differential-Algebraic Temporal Dynamic Logic (XZ, BL, MZ, JL, QC, SJ), pp. 231–234.
SEKESEKE-2012-ZhuLLCZJ #continuation #difference #logic #using
HybridUML Based Verification of CPS Using Differential Dynamic Logic (MZ, BL, JL, QC, XZ, SJ), pp. 235–238.
ECMFAECMFA-2012-GeP #framework #realtime #safety #uml
Time Properties Verification Framework for UML-MARTE Safety Critical Real-Time Systems (NG, MP), pp. 352–367.
ECMFAECMFA-2012-RadjenovicMPRMBK #automation #embedded #modelling #named #uml
MADES: A Tool Chain for Automated Verification of UML Models of Embedded Systems (AR, NDM, RFP, MR, AM, LB, DSK), pp. 340–351.
MODELSMoDELS-2012-ButtnerEC #atl #off the shelf #on the #smt #using
On Verifying ATL Transformations Using “off-the-shelf” SMT Solvers (FB, ME, JC), pp. 432–448.
SPLCSPLC-2012-CordySHL #behaviour #modelling #product line #realtime
Behavioural modelling and verification of real-time software product lines (MC, PYS, PH, AL), pp. 66–75.
ECOOPECOOP-2012-DiasDSL #java #memory management #source code #transaction
Verification of Snapshot Isolation in Transactional Memory Java Programs (RJD, DD, JCS, JL), pp. 640–664.
OOPSLAOOPSLA-2012-BettsCDQT #gpu #kernel #named
GPUVerify: a verifier for GPU kernels (AB, NC, AFD, SQ, PT), pp. 113–132.
TOOLSTOOLS-EUROPE-2012-MehnertA #type system #using
Verification of Snapshotable Trees Using Access Permissions and Typestate (HM, JA), pp. 187–201.
AdaEuropeAdaEurope-2012-FairbairnB #implementation
Implementing and Verifying EDF Preemption-Level Resource Control (MLF, AB), pp. 193–206.
HILTHILT-2012-BeltCHR #ada #automation #contract #using
Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan (JB, PC, JH, R), pp. 3–4.
HILTHILT-2012-Kanig #ada #testing
Leading-edge ada verification technologies: combining testing and verification with GNATTest and GNATProve — the hi-lite project (JK), pp. 5–6.
HILTHILT-2012-KanigSD #compilation #convergence #named
Hi-Lite: the convergence of compiler technology and program verification (JK, ES, CD), pp. 27–34.
HILTHILT-2012-Leino12a #proving #using #why
Program proving using intermediate verification languages (IVLs) like boogie and why3 (KRML), pp. 25–26.
LOPSTRLOPSTR-2012-SeghirB #array #program transformation #quantifier
Simplifying the Verification of Quantified Array Assertions via Code Transformation (MNS, MB), pp. 194–212.
PEPMPEPM-2012-Berger #metaprogramming #specification
Specification and verification of meta-programs (MB), pp. 3–4.
PLDIPLDI-2012-GrebenshchikovLPR #proving
Synthesizing software verifiers from proof rules (SG, NPL, CP, AR), pp. 405–416.
PLDIPLDI-2012-LeungGAGJL #gpu #kernel
Verifying GPU kernels by test amplification (AL, MG, YA, RG, RJ, SL), pp. 383–394.
POPLPOPL-2012-FarzanK #composition #concurrent #reasoning #source code
Verification of parameterized concurrent programs by modular reasoning about data and control (AF, ZK), pp. 297–308.
POPLPOPL-2012-LiangFF #concurrent #program transformation #simulation
A rely-guarantee-based simulation for verifying concurrent program transformations (HL, XF, MF), pp. 455–468.
PPDPPPDP-2012-OlartePRC #approach #automation #concurrent #constraints #linear
A linear concurrent constraint approach for the automatic verification of access permissions (CO, EP, CR, NC), pp. 207–216.
QAPLQAPL-2012-BelardinelliGL #automation #protocol #quantum #using
Automated Verification of Quantum Protocols using MCMAS (FB, PG, AL), pp. 48–62.
ASEASE-2012-BiallasBK #framework #logic #platform #programmable
Arcade.PLC: a verification platform for programmable logic controllers (SB, JB, SK), pp. 338–341.
ASEASE-2012-Gabmeyer #model transformation
Formal verification techniques for model transformations specified by-demonstration (SG), pp. 390–393.
ASEASE-2012-NijjarB #bound #smt #using
Unbounded data model verification using SMT solvers (JN, TB), pp. 210–219.
FSEFSE-2012-BeyerHKW #model checking
Conditional model checking: a technique to pass information between verifiers (DB, TAH, MEK, PW), p. 57.
FSEFSE-2012-NearJ #bound #named #web
Rubicon: bounded verification of web applications (JPN, DJ), p. 60.
FSEFSE-2012-ShaikhW #diagrams #ocl #performance #slicing #uml
UMLtoCSP (UOST): a tool for efficient verification of UML/OCL class diagrams through model slicing (AS, UKW), p. 37.
ICSEICSE-2012-AlkhalafBG #analysis #string #using #validation
Verifying client-side input validation functions using string analysis (MA, TB, JLG), pp. 947–957.
ICSEICSE-2012-AndronickJKKSZZ #perspective #process #scalability
Large-scale formal verification in practice: A process perspective (JA, DRJ, GK, RK, MS, HZ, LZ), pp. 1002–1011.
ICSEICSE-2012-CookHSS #compilation #composition #specification #using
Specification engineering and modular verification using a web-integrated verifying compiler (CTC, HKH, HS, MS), pp. 1379–1382.
ICSEICSE-2012-LutzLLKHMS #programmable #requirements #self
Engineering and verifying requirements for programmable self-assembling nanomachines (RRL, JHL, JIL, TK, EH, DM, DAS), pp. 1361–1364.
ICSEICSE-2012-Motta #modelling #multi #towards #uml
Towards the verification of multi-diagram UML models (AM), pp. 1531–1534.
SACSAC-2012-AtifMO #detection
Formal verification of Unreliable Failure Detectors in Partially Synchronous Systems (MA, MRM, AO), pp. 478–485.
SACSAC-2012-ChebaroKGJ #dynamic analysis #slicing
Program slicing enhances a verification technique combining static and dynamic analysis (OC, NK, AG, JJ), pp. 1284–1291.
SACSAC-2012-CruzFP #source code
Verification conditions for single-assignment programs (DCdC, MJF, JSP), pp. 1264–1270.
SACSAC-2012-LassaigneP #approximate #markov #process #scalability
Approximate planning and verification for large markov decision processes (RL, SP), pp. 1314–1319.
SACSAC-2012-SalaunEPBC #distributed #in the cloud #protocol #self
Verification of a self-configuration protocol for distributed applications in the cloud (GS, XE, NDP, FB, TC), pp. 1278–1283.
GPCEGPCE-2012-ThumSHA #deduction #product line
Family-based deductive verification of software product lines (TT, IS, MH, SA), pp. 11–20.
CASECASE-2012-KlotzSSFTS #on the
On the formal verification of routing in material handling systems (TK, NS, BS, EF, KT, JS), pp. 8–13.
CASECASE-2012-WimbockRC #coordination
Derivation and verification of synergy coordinates for the DLR hand arm system (TW, JR, MC), pp. 454–460.
DACDAC-2012-AbhishekN #grid #incremental #power management
Incremental power grid verification (A, FNN), pp. 151–156.
DACDAC-2012-KumarGCALT #approach #cyber-physical #hybrid
A hybrid approach to cyber-physical systems verification (PK, DG, SC, AA, KL, LT), pp. 688–696.
DACDAC-2012-LiSJ #crowdsourcing #named #towards
CrowdMine: towards crowdsourced human-assisted verification (WL, SAS, SJ), pp. 1254–1255.
DACDAC-2012-Seshia #deduction #induction #named #synthesis
Sciduction: combining induction, deduction, and structure for verification and synthesis (SAS), pp. 356–365.
DACDAC-2012-UrdahlSWK #abstraction #composition #concurrent
System verification of concurrent RTL modules by compositional path predicate abstraction (JU, DS, MW, WK), pp. 334–343.
DATEDATE-2012-Al-HashimiM #framework #hardware #platform #question
Accelerators and emulators: Can they become the platform of choice for hardware verification? (BMAH, RM), p. 430.
DATEDATE-2012-BeckerDFMPV #embedded #evolution #modelling #named #scalability
MOUSSE: Scaling modelling and verification to complex Heterogeneous Embedded Systems evolution (MB, GBD, FF, WM, GP, SV), pp. 296–299.
DATEDATE-2012-BombieriFG #fault #framework #functional #named #simulation
FAST-GP: An RTL functional verification framework based on fault simulation on GP-GPUs (NB, FF, VG), pp. 562–565.
DATEDATE-2012-DenizSH #embedded #manycore
Verification coverage of embedded multicore applications (ED, AS, JH), pp. 252–255.
DATEDATE-2012-GuglielmoGFP #design #embedded #modelling
Enabling dynamic assertion-based verification of embedded software through model-driven design (GDG, LDG, FF, GP), pp. 212–217.
DATEDATE-2012-HaedickeGD #metric
A guiding coverage metric for formal verification (FH, DG, RD), pp. 617–622.
DATEDATE-2012-HammamiLB #named #network
NOCEVE: Network on chip emulation and verification environment (OH, XL, JMB), pp. 163–164.
DATEDATE-2012-JongheMGMTS #modelling #roadmap #testing
Advances in variation-aware modeling, verification, and testing of analog ICs (DdJ, EM, GGEG, TM, BT, HGDS), pp. 1615–1620.
DATEDATE-2012-LvKE #multi #performance #reduction
Efficient Gröbner basis reductions for formal verification of galois field multipliers (JL, PK, FE), pp. 899–904.
DATEDATE-2012-MarinMLB #design #incremental #using
Verification of partial designs using incremental QBF solving (PM, CM, MDTL, BB), pp. 623–628.
DATEDATE-2012-NarayananDZT #design #using
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
Verifying timing synchronization constraints in distributed embedded architectures (ACR, SM, SR), pp. 200–205.
DATEDATE-2012-RamboHS #consistency #memory management #multi #on the
On ESL verification of memory consistency for system-on-chip multiprocessing (EAR, OPH, LCVdS), pp. 9–14.
DATEDATE-2012-RayB #scalability
Scalable progress verification in credit-based flow-control systems (SR, RKB), pp. 905–910.
DATEDATE-2012-YipHI #3d #challenge #design
Challenges in verifying an integrated 3D design (TGY, CYH, VI), pp. 167–168.
DATEDATE-2012-YordanovAGGCBHBD #biology
Experimentally driven verification of synthetic biological circuits (BY, EA, RG, EAG, SBC, SB, TH, CB, DD), pp. 236–241.
PPoPPPPoPP-2012-LiLSGGR #generative #named #testing
GKLEE: concolic verification and test generation for GPUs (GL, PL, GS, GG, IG, SPR), pp. 215–224.
PPoPPPPoPP-2012-MalkisB
Verification of software barriers (AM, AB), pp. 313–314.
ESOPESOP-2012-ChadhaCK #automation #encryption #equivalence #protocol
Automated Verification of Equivalence Properties of Cryptographic Protocols (RC, SC, SK), pp. 108–127.
FASEFASE-2012-HatvaniPS #adaptation #automaton #embedded #framework
Adaptive Task Automata: A Framework for Verifying Adaptive Embedded Systems (LH, PP, CCS), pp. 115–129.
TACASTACAS-2012-BaslerDKKTW #c #contest #named #source code
satabs: A Bit-Precise Verifier for C Programs — (Competition Contribution) (GB, AFD, AK, DK, MT, TW), pp. 552–555.
TACASTACAS-2012-Beyer #contest
Competition on Software Verification — (SV-COMP) (DB0), pp. 504–524.
TACASTACAS-2012-ChenFKPS #automation #probability
Automatic Verification of Competitive Stochastic Systems (TC, VF, MZK, DP, AS), pp. 315–330.
TACASTACAS-2012-CoxSC #bound #precise
A Bit Too Precise? Bounded Verification of Quantized Digital Filters (AC, SS, BYEC), pp. 33–47.
TACASTACAS-2012-DudkaMPV #contest #data type #linked data #named #open data #source code
Predator: A Verification Tool for Programs with Dynamic Linked Data Structures — (Competition Contribution) (KD, PM, PP, TV), pp. 545–548.
TACASTACAS-2012-GrebenshchikovGLPR #contest #horn clause
HSF(C): A Software Verifier Based on Horn Clauses — (Competition Contribution) (SG, AG, NPL, CP, AR), pp. 549–551.
TACASTACAS-2012-HardinSWP
The Guardol Language and Verification System (DSH, KS, MWW, THP), pp. 18–32.
TACASTACAS-2012-HeussnerGS #communication #framework #named
McScM: A General Framework for the Verification of Communicating Machines (AH, TLG, GS), pp. 478–484.
TACASTACAS-2012-HolzlN #model checking
Verifying pCTL Model Checking (JH, TN), pp. 347–361.
TACASTACAS-2012-JiangPMAM #modelling
Modeling and Verification of a Dual Chamber Implantable Pacemaker (ZJ, MP, SM, RA, RM), pp. 188–203.
TACASTACAS-2012-YehWH #design #framework #named #open source #synthesis #towards
QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification (HHY, CYW, CY(H), pp. 377–391.
CAVCAV-2012-AlbarghouthiLGC #framework #named
Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification (AA, YL, AG, MC), pp. 672–678.
CAVCAV-2012-Bradley #incremental #induction
IC3 and beyond: Incremental, Inductive Verification (ARB), p. 4.
CAVCAV-2012-ChuJ #reduction #safety #symmetry
A Complete Method for Symmetry Reduction in Safety Verification (DHC, JJ), pp. 616–633.
CAVCAV-2012-CimattiCLNRRST #industrial #validation
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System (AC, RC, AL, IN, TR, MR, AS, AT), pp. 378–393.
CAVCAV-2012-JaffarMNS #execution #named #symbolic computation
TRACER: A Symbolic Execution Tool for Verification (JJ, VM, JAN, AES), pp. 758–766.
CAVCAV-2012-Moskal #bound #c #infinity
From C to Infinity and Back: Unbounded Auto-active Verification with VCC (MM), p. 6.
CAVCAV-2012-Myers #search-based
Formal Verification of Genetic Circuits (CJM), p. 5.
CAVCAV-2012-RondonBKJ #c #named
CSolve: Verifying C with Liquid Types (PMR, AB, MK, RJ), pp. 744–750.
ICSTICST-2012-AmraniLSCDVTC #approach #model transformation
A Tridimensional Approach for Studying the Formal Verification of Model Transformations (MA, LL, GMKS, BC, JD, HV, YLT, JRC), pp. 921–928.
ICSTICST-2012-LiuNT #bound #case study #smt #using
Bounded Program Verification Using an SMT Solver: A Case Study (TL, MN, MT), pp. 101–110.
ICSTICST-2012-SalayCG #towards
Towards a Methodology for Verifying Partial Model Refinements (RS, MC, JG), pp. 938–945.
ICSTICST-2012-TranP #framework #graph transformation #towards
Towards a Rule-Level Verification Framework for Property-Preserving Graph Transformations (HNT, CP), pp. 946–953.
IJCARIJCAR-2012-BoerBR #automation #pointer #recursion #source code
Automated Verification of Recursive Programs with Pointers (FSdB, MMB, JR), pp. 149–163.
IJCARIJCAR-2012-JacquelBDD #automation #deduction #modulo theories #proving #theorem proving #using
Tableaux Modulo Theories Using Superdeduction — An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover (MJ, KB, DD, CD), pp. 332–338.
LICSLICS-2012-AgrawalAGT #approximate #markov
Approximate Verification of the Symbolic Dynamics of Markov Chains (MA, SA, BG, PST), pp. 55–64.
LICSLICS-2012-EsparzaGM #bound
A Perfect Model for Bounded Verification (JE, PG, RM), pp. 285–294.
SMTSMT-2012-BjornerMR #modulo theories #satisfiability
Program Verification as Satisfiability Modulo Theories (NB, KLM, AR), pp. 3–11.
SMTSMT-2012-GoelKLT #smt
SMT-Based System Verification with DVF (AG, SK, RL, MRT), pp. 32–43.
TAPTAP-2012-KiniryZH #consistency #library #specification #testing
Testing Library Specifications by Verifying Conformance Tests (JRK, DMZ, RH), pp. 51–66.
VMCAIVMCAI-2012-AlbarghouthiGC #algorithm #interprocedural #named
Whale: An Interpolation-Based Algorithm for Inter-procedural Verification (AA, AG, MC), pp. 39–55.
VMCAIVMCAI-2012-BasuBO #communication
Synchronizability for Verification of Asynchronously Communicating Systems (SB, TB, MO), pp. 56–71.
VMCAIVMCAI-2012-BozzelliP #abstraction #constraints
Verification of Gap-Order Constraint Abstractions of Counter Systems (LB, SP), pp. 88–103.
VMCAIVMCAI-2012-ChakiGS #concurrent #multi #source code #thread
Regression Verification for Multi-threaded Programs (SC, AG, OS), pp. 119–135.
VMCAIVMCAI-2012-CharltonHR #higher-order #named #source code
Crowfoot: A Verifier for Higher-Order Store Programs (NC, BH, BR), pp. 136–151.
VMCAIVMCAI-2012-Jhala
Software Verification with Liquid Types (RJ), p. 23.
VMCAIVMCAI-2012-NamjoshiT #composition #symmetry
Local Symmetry and Compositional Verification (KSN, RJT), pp. 348–362.
ECSAECSA-2011-HamelGKBG #behaviour #transaction
Verifying Composite Service Transactional Behavior with EVENT-B (LH, MG, MK, MTB, WG), pp. 67–74.
ECSAECSA-2011-JohnsenPL #architecture #specification
An Architecture-Based Verification Technique for AADL Specifications (AJ, PP, KL), pp. 105–113.
ICDARICDAR-2011-BeusekomS #automation #documentation #metric
Distortion Measurement for Automatic Document Verification (JvB, FS), pp. 289–293.
ICDARICDAR-2011-LiwickiMHCBSBF #contest #online
Signature Verification Competition for Online and Offline Skilled Forgeries (SigComp2011) (ML, MIM, CEvdH, XC, CB, RS, MB, BF), pp. 1480–1484.
ICDARICDAR-2011-NguyenB #2d #feature model
An Application of the 2D Gaussian Filter for Enhancing Feature Extraction in Off-line Signature Verification (VN, MB), pp. 339–343.
ICDARICDAR-2011-NobileHSLS
Digit/Symbol Pruning and Verification for Arabic Handwritten Digit/Symbol Spotting (NN, CLH, MWS, LL, CYS), pp. 648–652.
ICDARICDAR-2011-PanZSN11a #adaptation #detection #segmentation
Improving Scene Text Detection by Scale-Adaptive Segmentation and Weighted CRF Verification (YFP, YZ, JS, SN), pp. 759–763.
ICDARICDAR-2011-ParodiGB #approach #feature model #invariant
A Circular Grid-Based Rotation Invariant Feature Extraction Approach for Off-line Signature Verification (MP, JCG, AB), pp. 1289–1293.
ICDARICDAR-2011-WangWZ #graph #online #using
On-line Signature Verification Using Segment-to-Segment Graph Matching (KW, YW, ZZ), pp. 804–808.
VLDBVLDB-2012-CormodeTY11 #interactive #proving #streaming
Verifying Computations with Streaming Interactive Proofs (GC, JT, KY), pp. 25–36.
CSEETCSEET-2011-LiB #education #process #re-engineering #research #validation
Making winners for both education and research: Verification and validation process improvement practice in a software engineering course (QL, BWB), pp. 304–313.
ITiCSEITiCSE-2011-VirsedaM #debugging #education #semantics #source code
An innovative teaching tool based on semantic tableaux for verification and debugging of programs (RdVV, FPM), p. 352.
CIAACIAA-J-2010-YuBI11 #automaton #multi #relational #string #using
Relational String Verification Using Multi-Track Automata (FY, TB, OHI), pp. 1909–1924.
FMFM-2011-BartheBCL
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization (GB, GB, JDC, CL), pp. 231–245.
FMFM-2011-BartheCK #relational #source code #using
Relational Verification Using Product Programs (GB, JMC, CK), pp. 200–214.
FMFM-2011-BonakdarpourNF #runtime
Sampling-Based Runtime Verification (BB, SN, SF), pp. 88–102.
FMFM-2011-BoyerGS #configuration management #protocol #specification
Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP (FB, OG, GS), pp. 103–117.
FMFM-2011-DerrickSW
Verifying Linearisability with Potential Linearisation Points (JD, GS, HW), pp. 323–337.
FMFM-2011-DietschWP
System Verification through Program Verification (DD, BW, AP), pp. 27–41.
FMFM-2011-GherghinaDQC #source code #specification
Structured Specifications for Better Verification of Heap-Manipulating Programs (CG, CD, SQ, WNC), pp. 386–401.
FMFM-2011-HaxthausenKB #automation #development #modelling
Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems (AEH, AAK, MLB), pp. 118–132.
FMFM-2011-JacobsSP
Verification of Unloadable Modules (BJ, JS, FP), pp. 402–416.
FMFM-2011-MeryMT #algorithm
Refinement-Based Verification of Local Synchronization Algorithms (DM, MM, MT), pp. 338–352.
FMFM-2011-MullerR #using
Using Debuggers to Understand Failed Verification Attempts (PM, JNR), pp. 73–87.
FMFM-2011-QinLCH #automation #specification
Automatically Refining Partial Specifications for Program Verification (SQ, CL, WNC, GH), pp. 369–385.
SEFMSEFM-2011-BlechB #coq #semantics
Verification of PLC Properties Based on Formal Semantics in Coq (JOB, SOB), pp. 58–73.
SEFMSEFM-2011-BubelHG #formal method #java #specification #string
A Formalisation of Java Strings for Program Specification and Verification (RB, RH, UG), pp. 90–105.
SEFMSEFM-2011-CastroKAA #branch #fault tolerance #logic #named
dCTL: A Branching Time Temporal Logic for Fault-Tolerant System Verification (PFC, CK, AA, NA), pp. 106–121.
SEFMSEFM-2011-ErnstSR #analysis #empirical #interactive #proving #theorem proving
Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving (GE, GS, WR), pp. 188–203.
SEFMSEFM-2011-FalconeJNBB #component #runtime
Runtime Verification of Component-Based Systems (YF, MJ, THN, MB, SB), pp. 204–220.
SEFMSEFM-2011-GouesLM #debugging
The Boogie Verification Debugger (CLG, KRML, MM), pp. 407–414.
SEFMSEFM-2011-JacquelBDD #automation #proving #theorem proving #using
Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (MJ, KB, DD, CD), pp. 253–268.
SEFMSEFM-2011-ParrinoGGF #analysis #bound #data flow #satisfiability
A Dataflow Analysis to Improve SAT-Based Bounded Program Verification (BCP, JPG, DG, MFF), pp. 138–154.
SEFMSEFM-2011-SoleimanifardGH #composition #named #safety
ProMoVer: Modular Verification of Temporal Safety Properties (SS, DG, MH), pp. 366–381.
SEFMSEFM-2011-TschannenFNM #object-oriented #source code
Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques (JT, CAF, MN, BM), pp. 382–398.
SFMSFM-2011-BaierKK #component #modelling
Modeling and Verification of Components and Connectors (CB, JK, SK), pp. 114–147.
SFMSFM-2011-ForejtKNP #automation #probability
Automated Verification Techniques for Probabilistic Systems (VF, MZK, GN, DP), pp. 53–113.
ICFPICFP-2011-Chargueraud #imperative #source code
Characteristic formulae for the verification of imperative programs (AC), pp. 418–430.
ICFPICFP-2011-GotsmanY #composition #kernel
Modular verification of preemptive OS kernels (AG, HY), pp. 404–417.
IFLIFL-2011-Page #testing
Property-Based Testing and Verification: A Catalog of Classroom Examples (RP), pp. 134–147.
HCIHCI-ITE-2011-LinD #modelling
Verification of Two Models of Ballistic Movements (JFL, CGD), pp. 275–284.
HCIHCI-MIIE-2011-RiahiRM #generative #human-computer #mobile #specification #xml
XML in Formal Specification, Verification and Generation of Mobile HCI (IR, MR, FM), pp. 92–100.
ICEISICEIS-v3-2011-LinLMZN #approach #workflow
Approach for Verifying Workflow Validity (YL, TL, IM, RZ, RN), pp. 66–75.
KEODKEOD-2011-KhuratS #approach #ontology #policy
An Ontological Approach to Verifying P3P Policies (AK, BS), pp. 349–353.
SEKESEKE-2011-DengLSW #api #constraints #runtime #specification
Specification and Runtime Verification of API Constraints on Interacting Objects (FD, HL, JS, QW), pp. 101–106.
ECMFAECMFA-2011-CariouBFB #contract #execution
Contracts for Model Execution Verification (EC, CB, AF, FB), pp. 3–18.
ECMFAECMFA-2011-ElaasarBL #qvt
Domain-Specific Model Verification with QVT (ME, LCB, YL), pp. 282–298.
ECMFAECMFA-2011-JurjensMOS #evolution #incremental #modelling #security
Incremental Security Verification for Evolving UMLsec models (JJ, LM, MO, HS), pp. 52–68.
MODELSMoDELS-2011-MoffettBD #consistency #model checking #protocol #uml #using
Verifying UML-RT Protocol Conformance Using Model Checking (YM, AB, JD), pp. 410–424.
MODELSMoDELS-2011-StenzelMR #code generation #qvt
Formal Verification of QVT Transformations for Code Generation (KS, NM, WR), pp. 533–547.
SPLCSPLC-2011-GhezziS #approach #model checking #non-functional #parametricity #performance #product line #towards #using
Verifying Non-functional Properties of Software Product Lines: Towards an Efficient Approach Using Parametric Model Checking (CG, AMS), pp. 170–174.
ECOOPECOOP-2011-BalzerG #invariant #multi
Verifying Multi-object Invariants with Relationships (SB, TRG), pp. 358–382.
OnwardOnward-2011-Bierhoff #automation #lightweight #reasoning
Automated program verification made SYMPLAR: symbolic permissions for lightweight automated reasoning (KB), pp. 19–32.
OOPSLAOOPSLA-2011-DavidC #precise #specification
Immutable specifications for more concise and precise verification (CD, WNC), pp. 359–374.
OOPSLAOOPSLA-2011-MadhavanK #analysis #approximate #null
Null dereference verification via over-approximated weakest pre-conditions analysis (RM, RK), pp. 1033–1052.
AdaEuropeAdaEurope-2011-CarnevaliLPV #approach #design #formal method #scheduling
A Formal Approach to Design and Verification of Two-Level Hierarchical Scheduling Systems (LC, GL, AP, EV), pp. 118–131.
PLDIPLDI-2011-Chlipala #logic #low level #source code
Mostly-automated verification of low-level programs in computational separation logic (AC), pp. 234–245.
PLDIPLDI-2011-KimR #commutative #data type #linked data #open data #semantics
Verification of semantic commutativity conditions and inverse operations on linked data structures (DK, MCR), pp. 528–541.
POPLPOPL-2011-AlurC #algorithm #source code #streaming #transducer
Streaming transducers for algorithmic verification of single-pass list-processing programs (RA, PC), pp. 599–610.
POPLPOPL-2011-EsparzaG #complexity #parallel #source code #thread
Complexity of pattern-based verification for multithreaded programs (JE, PG), pp. 499–510.
POPLPOPL-2011-GordonHHJS #concurrent
Robin Milner 1934--2010: verification, languages, and concurrency (ADG, RH, JH, AJ, PS), pp. 473–474.
POPLPOPL-2011-GuptaPR #abstraction #concurrent #multi #refinement #source code #thread
Predicate abstraction and refinement for verifying multi-threaded programs (AG, CP, AR), pp. 331–344.
POPLPOPL-2011-OngR #algebra #data type #functional #higher-order #pattern matching #source code
Verifying higher-order functional programs with pattern-matching algebraic data types (CHLO, SJR), pp. 587–598.
POPLPOPL-2011-RamananandroRL #c++ #inheritance #layout #multi
Formal verification of object layout for c++ multiple inheritance (TR, GDR, XL), pp. 67–80.
PPDPPPDP-2011-InabaHHKN #higher-order #logic #monad #using
Graph-transformation verification using monadic second-order logic (KI, SH, ZH, HK, KN), pp. 17–28.
PPDPPPDP-2011-Rybalchenko #automation #synthesis #tool support #towards
Towards automatic synthesis of software verification tools (AR), pp. 3–4.
SASSAS-2011-DonaldsonHKR #using
Software Verification Using k-Induction (AFD, LH, DK, PR), pp. 351–368.
SASSAS-2011-SchrammelJ #data flow #source code
Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs (PS, BJ), pp. 233–248.
SASSAS-2011-VafeiadisN #optimisation
Verifying Fence Elimination Optimisations (VV, FZN), pp. 146–162.
ASEASE-2011-ApelSWRB #detection #feature model #interactive #using
Detection of feature interactions using feature-aware verification (SA, HS, PW, AvR, DB), pp. 372–375.
ASEASE-2011-IvancicBGSMTIM #bound #framework #named #scalability
DC2: A framework for scalable, scope-bounded software verification (FI, GB, AG, SS, NM, HT, TI, YM), pp. 133–142.
ESEC-FSEESEC-FSE-2011-Filieri #runtime
QoS verification and model tuning @ runtime (AF), pp. 408–411.
ESEC-FSEESEC-FSE-2011-MontrieuxWY #data access #specification #tool support #uml
Tool support for UML-based specification and verification of role-based access control properties (LM, MW, YY), pp. 456–459.
ESEC-FSEESEC-FSE-2011-NaudziunieneBDDGP #automation #ide #java #named #source code
jStar-eclipse: an IDE for automated verification of Java programs (DN, MB, DD, MD, RG, MJP), pp. 428–431.
ICSEICSE-2011-CassouBCL #architecture #development
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
Verifying multi-threaded software using smt-based context-bounded model checking (LC, BF), pp. 331–340.
ICSEICSE-2011-GeTXT #execution #named #symbolic computation
DyTa: dynamic symbolic execution guided with static verification results (XG, KT, TX, NT), pp. 992–994.
ICSEICSE-2011-RosuS #approach #logic
Matching logic: a new program verification approach (GR, AS), pp. 868–871.
SACSAC-2011-ChangH #approach #model transformation #multi #using
A model transformation approach for verifying multi-agent systems using SPIN (LC, XH), pp. 37–42.
SACSAC-2011-ChuHLCHC #approach #development #manycore
A pattern-based verification approach for a multi-core system development (PHC, NLH, CCL, MJC, PAH, WCC), pp. 49–53.
SACSAC-2011-DumasDBB #partial order
Application of partial-order methods for the verification of closed-loop SDL systems (XD, PD, FB, EB), pp. 1666–1673.
SACSAC-2011-MammarFD #approach #reachability
A proof-based approach to verifying reachability properties (AM, MF, FD), pp. 1651–1657.
SACSAC-2011-Muramatsu #algorithm #online #random
Random forgery attacks against DTW-based online signature verification algorithm (DM), pp. 27–28.
SACSAC-2011-RayNDF #interactive #privacy
Verification of data pattern for interactive privacy preservation model (SR, MFN, SD, BCMF), pp. 1716–1723.
SACSAC-2011-ZhuWHAHY #outsourcing
Dynamic audit services for integrity verification of outsourced storages in clouds (YZ, HW, ZH, GJA, HH, SSY), pp. 1550–1557.
GPCEGPCE-2011-SlattenKH #automation #case study #distributed #generative #industrial #reliability #specification #towards #validation
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.
ASPLOSASPLOS-2011-RyzhykKMRVH #hardware #reliability #reuse
Improved device driver reliability through hardware verification reuse (LR, JK, BM, AR, MV, GH), pp. 133–144.
CASECASE-2011-BallariniDDHP #composition #flexibility #modelling #petri net
Petri nets compositional modeling and verification of Flexible Manufacturing Systems (PB, HD, MD, SH, NP), pp. 588–593.
CASECASE-2011-ThramboulidisSF #automation #industrial #process #safety #towards
Towards an automated verification process for industrial safety applications (KT, DS, GF), pp. 482–487.
CGOCGO-2011-Leroy #compilation #how #question #why
Formally verifying a compiler: Why? How? How far? (XL).
DACDAC-2011-AdirNSZMS #validation
Leveraging pre-silicon verification resources for the post-silicon validation of the IBM POWER7 processor (AA, AN, GS, AZ, CM, JS), pp. 569–574.
DACDAC-2011-GhaniN #branch #grid #power management #using
Power grid verification using node and branch dominance (NHAG, FNN), pp. 682–687.
DACDAC-2011-HolcombBS #performance
Abstraction-based performance verification of NoCs (DEH, BAB, SAS), pp. 492–497.
DACDAC-2011-KadryMGAK #approach #challenge #design #effectiveness
Facing the challenge of new design features: an effective verification approach (WK, RM, AG, EA, CAK), pp. 842–847.
DACDAC-2011-MoffittSV #clustering #functional #robust
Robust partitioning for hardware-accelerated functional verification (MDM, MAS, PGV), pp. 854–859.
DACDAC-2011-RameshG #design #modelling
Rigorous model-based design & verification flow for in-vehicle software (SR, AAG), pp. 13–16.
DATEDATE-2011-AdirCLNSZMS #validation
A unified methodology for pre-silicon verification and post-silicon validation (AA, SC, SL, AN, GS, AZ, CM, JS), pp. 1590–1595.
DATEDATE-2011-BehrendLHRKR #embedded #hybrid #scalability
Scalable hybrid verification for embedded software (JB, DL, PH, JR, TK, WR), pp. 179–184.
DATEDATE-2011-CroneBCDER #state of the art
State of the art verification methodologies in 2015 (AC, OB, CC, BD, VE, MR), p. 1339.
DATEDATE-2011-GoyalN #grid #performance #power management #using
Efficient RC power grid verification using node elimination (AG, FNN), pp. 257–260.
DATEDATE-2011-GuoCSCWH #debugging #design #empirical #predict
Empirical design bugs prediction for verification (QG, TC, HS, YC, YW, WH), pp. 161–166.
DATEDATE-2011-JhaLMR #simulation #statistics #trade-off
When to stop verification?: Statistical trade-off between expected loss and simulation cost (SKJ, CJL, SM, SR), pp. 1309–1314.
DATEDATE-2011-KapoorHT #case study #experience #power management
Power management verification experiences in Wireless SoCs (BK, AH, PT), pp. 507–508.
DATEDATE-2011-KapoorJ #design #embedded #power management #tutorial
Embedded tutorial: Addressing critical power management verification issues in low power designs (BK, KMJ), p. 124.
DATEDATE-2011-MatsudaI #debugging
Developing an integrated verification and debug methodology (AM, TI), pp. 503–504.
DATEDATE-2011-PangrleBCDJ #design #power management
Beyond UPF & CPF: Low-power design and verification (BMP, JB, CC, OD, KMJ), p. 252.
DATEDATE-2011-PavlenkoWSKDSG #algebra #named #problem #reasoning #smt
STABLE: A new QF-BV SMT solver for hard verification problems combining Boolean reasoning with computer algebra (EP, MW, DS, WK, AD, FS, GMG), pp. 155–160.
DATEDATE-2011-SoekenWD #aspect-oriented #modelling #uml
Verifying dynamic aspects of UML models (MS, RW, RD), pp. 1077–1082.
PPoPPPPoPP-2011-SiegelZ #automation #parallel #source code
Automatic formal verification of MPI-based parallel programs (SFS, TKZ), pp. 309–310.
FoSSaCSFoSSaCS-2011-DelzannoSZ #ad hoc #clique #network #on the #power of
On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks (GD, AS, GZ), pp. 441–455.
STOCSTOC-2011-SarmaHKKNPPW #approximate #distributed
Distributed verification and hardness of distributed approximation (ADS, SH, LK, AK, DN, GP, DP, RW), pp. 363–372.
TACASTACAS-2011-ForejtKNPQ #multi #probability
Quantitative Multi-objective Verification for Probabilistic Systems (VF, MZK, GN, DP, HQ), pp. 112–127.
TACASTACAS-2011-RavnSV #modelling #process #protocol #web #web service
Modelling and Verification of Web Services Business Activity Protocol (APR, JS, SV), pp. 357–371.
CAVCAV-2011-AlkassarBMR
Verification of Certifying Computations (EA, SB, KM, CR), pp. 67–82.
CAVCAV-2011-BeyerK #configuration management #named
CPAchecker: A Tool for Configurable Software Verification (DB, MEK), pp. 184–190.
CAVCAV-2011-ChinGVLCQ #calculus
A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification (WNC, CG, RV, QLL, FC, SQ), pp. 293–309.
CAVCAV-2011-CimattiMT #automaton #hybrid #performance
Efficient Scenario Verification for Hybrid Automata (AC, SM, ST), pp. 317–332.
CAVCAV-2011-CookKV #program analysis
Temporal Property Verification as a Program Analysis Task (BC, EK, MYV), pp. 333–348.
CAVCAV-2011-FrehseGDCRLRGDM #hybrid #named #scalability
SpaceEx: Scalable Verification of Hybrid Systems (GF, CLG, AD, SC, RR, OL, RR, AG, TD, OM), pp. 379–395.
CAVCAV-2011-GuptaPR #concurrent #constraints #multi #named #source code #thread
Threader: A Constraint-Based Verifier for Multi-threaded Programs (AG, CP, AR), pp. 412–417.
CAVCAV-2011-HabermehlHRSV #automaton
Forest Automata for Verification of Heap Manipulation (PH, LH, AR, JS, TV), pp. 424–440.
CAVCAV-2011-Jhala #using
Using Types for Software Verification (RJ), p. 20.
CAVCAV-2011-JhalaMR #functional #named #source code #using
HMC: Verifying Functional Programs Using Abstract Interpreters (RJ, RM, AR), pp. 470–485.
CAVCAV-2011-KleinN #automation #behaviour #formal method #rest
Formalization and Automated Verification of RESTful Behavior (UK, KSN), pp. 541–556.
CAVCAV-2011-KroeningW
Interpolation-Based Software Verification with Wolverine (DK, GW), pp. 573–578.
CAVCAV-2011-KwiatkowskaNP #probability #realtime
PRISM 4.0: Verification of Probabilistic Real-Time Systems (MZK, GN, DP), pp. 585–591.
CAVCAV-2011-MullerP #hardware #interface
Complete Formal Hardware Verification of Interfaces for a FlexRay-Like Bus (CAM, WJP), pp. 633–648.
CAVCAV-2011-PeterEM #automaton #named #synthesis
Synthia: Verification and Synthesis for Timed Automata (HJP, RE, RM), pp. 649–655.
CAVCAV-2011-Platzer #composition #hybrid #logic
Logic and Compositional Verification of Hybrid Systems — (AP), pp. 28–43.
CAVCAV-2011-RamosE #equivalence
Practical, Low-Effort Equivalence Verification of Real Code (DAR, DRE), pp. 669–685.
CAVCAV-2011-SinghalA #simulation #using
Using Coverage to Deploy Formal Verification in a Simulation World (VS, PA), pp. 44–49.
ICSTICST-2011-Bhattacharya #hybrid
SoftwareHardware Hybrid Systems Verification (NB), pp. 435–438.
ICSTICST-2011-RubanovS #kernel #linux #runtime
Runtime Verification of Linux Kernel Modules Based on Call Interception (VVR, EAS), pp. 180–189.
ISSTAISSTA-2011-NijjarB #bound #modelling #ruby
Bounded verification of Ruby on Rails data models (JN, TB), pp. 67–77.
LICSLICS-2011-GollerL #complexity #term rewriting
The Complexity of Verifying Ground Tree Rewrite Systems (SG, AWL), pp. 279–288.
TAPTAP-2011-SoekenWD #data type #encoding #modelling #ocl #satisfiability #uml
Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models (MS, RW, RD), pp. 152–170.
VMCAIVMCAI-2011-GotmanovCK #communication
Verifying Deadlock-Freedom of Communication Fabrics (AG, SC, MK), pp. 214–231.
VMCAIVMCAI-2011-Logozzo #abstract interpretation
Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation — (FL), pp. 19–22.
ICSMEICSM-2010-KellensNDJP #cobol #design #outsourcing
Verifying the design of an outsourced COBOL system with IntensiVE (AK, CN, TD, LJ, BVP), pp. 1–8.
ICSMEICSM-2010-PonsiniCFMR #automation #invariant
Automatic verification of loop invariants (OP, HC, CF, CM, MR), pp. 1–5.
CIAACIAA-2010-YuBI #automaton #multi #relational #string #using
Relational String Verification Using Multi-track Automata (FY, TB, OHI), pp. 290–299.
ICALPICALP-v1-2010-ApplebaumIK #performance
From Secrecy to Soundness: Efficient Verification via Secure Computation (BA, YI, EK), pp. 152–163.
ICALPICALP-v2-2010-Goubault-Larrecq
Noetherian Spaces in Verification (JGL), pp. 2–21.
ICALPICALP-v2-2010-OuaknineW #bound #formal method #towards
Towards a Theory of Time-Bounded Verification (JO, JW), pp. 22–37.
LATALATA-2010-SaeedloeiG #induction #realtime
Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R) (NS, GG), pp. 536–548.
IFMIFM-2010-AutexierL #c #impact analysis #source code
Adding Change Impact Analysis to the Formal Verification of C Programs (SA, CL), pp. 59–73.
IFMIFM-2010-Faber #architecture #composition #realtime #reasoning
Verification Architectures: Compositional Reasoning for Real-Time Systems (JF), pp. 136–151.
IFMIFM-2010-FaberIJS #automation #parametricity #specification
Automatic Verification of Parametric Specifications with Complex Topologies (JF, CI, SJ, VSS), pp. 152–167.
IFMIFM-2010-LanoR #model transformation #specification #uml #using
Specification and Verification of Model Transformations Using UML-RSDS (KL, SKR), pp. 199–214.
SEFMSEFM-2010-BersaniCFPR #constraints #integer #ltl #runtime #smt #specification
SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability (MMB, LC, AF, MP, MR), pp. 244–254.
SEFMSEFM-2010-GallardoS #calculus #μ-calculus
Verification of Dynamic Data Tree with μ-calculus Extended with Separation (MdMG, DS), pp. 211–221.
SEFMSEFM-2010-Ghezzi #adaptation
Adaptive Software Needs Continuous Verification (CG), pp. 3–4.
SEFMSEFM-2010-Giannakopoulou #quote
“Fly Me to the Moon”: Verification of Aerospace Systems (DG), pp. 5–11.
SEFMSEFM-2010-GothelG #automation #invariant #network #realtime #towards #using
Towards the Semi-Automatic Verification of Parameterized Real-Time Systems Using Network Invariants (TG, SG), pp. 310–314.
ICFPICFP-2010-ArnoldHKBS #matrix #specification
Specifying and verifying sparse matrix codes (GA, JH, ASK, RB, MS), pp. 249–260.
ICFPICFP-2010-Chargueraud
Program verification through characteristic formulae (AC), pp. 321–332.
GT-VMTGT-VMT-2010-Schatz #model transformation
Verification of Model Transformations (BS).
ICGTICGT-2010-Blume #graph
Recognizable Graph Languages for the Verification of Dynamic Systems (CB), pp. 384–387.
ICGTICGT-2010-KonigE #graph transformation #specification
Verification of Graph Transformation Systems with Context-Free Specifications (BK, JE), pp. 107–122.
ICGTICGT-2010-Zambon #abstraction #graph transformation #using
Using Graph Transformations and Graph Abstractions for Software Verification (EZ), pp. 416–418.
CAiSECAiSE-2010-LyRD #design #graph #information management
Design and Verification of Instantiable Compliance Rule Graphs in Process-Aware Information Systems (LTL, SRM, PD), pp. 9–23.
ICEISICEIS-ISAS-2010-MoralesTP #composition #process
Compositional Verification of Business Processes Modelled with BPMN (LEMM, MICT, MAP), pp. 113–122.
ICEISICEIS-J-2010-MoralesTP10a #composition #formal method #process
A Formalization Proposal of Timed BPMN for Compositional Verification of Business Processes (LEMM, MICT, MAP), pp. 388–403.
ICPRICPR-2010-BatistaGS #difference #representation
Applying Dissimilarity Representation to Off-Line Signature Verification (LB, EG, RS), pp. 1293–1297.
ICPRICPR-2010-BourlaiKRCH
Cross-Spectral Face Verification in the Short Wave Infrared (SWIR) Band (TB, NDK, AR, BC, LH), pp. 1343–1347.
ICPRICPR-2010-BrewC
Vector Quantization Mappings for Speaker Verification (AB, PC), pp. 560–564.
ICPRICPR-2010-BuyssensR #learning
Learning Sparse Face Features: Application to Face Verification (PB, MR), pp. 670–673.
ICPRICPR-2010-GaoEFS #multi
Multi-resolution Local Appearance-Based Face Verification (HG, HKE, MF, RS), pp. 1501–1504.
ICPRICPR-2010-GuichardTC #novel #recognition #word
A Novel Verification System for Handwritten Words Recognition (LG, AHT, BC), pp. 2869–2872.
ICPRICPR-2010-HeLS #automation #recognition
Automatic Discrimination between Confusing Classes with Writing Styles Verification in Arabic Handwritten Numeral Recognition (CLH, LL, CYS), pp. 2045–2048.
ICPRICPR-2010-HendrikseVS
Verification Under Increasing Dimensionality (AH, RNJV, LJS), pp. 589–592.
ICPRICPR-2010-IbrahimKKG #analysis #online #using
On-Line Signature Verification Using 1-D Velocity-Based Directional Analysis (MTI, MJK, MAK, LG), pp. 3830–3833.
ICPRICPR-2010-Lei #distance #using
Combining the Likelihood and the Kullback-Leibler Distance in Estimating the Universal Background Model for Speaker Verification Using SVM (ZL), pp. 4553–4556.
ICPRICPR-2010-LiD #classification #multi
Multi-classifier Q-stack Aging Model for Adult Face Verification (WL, AD), pp. 1310–1313.
ICPRICPR-2010-LvBYD #using #visual notation
Off-Line Signature Verification Using Graphical Model (HL, XB, WY, JD), pp. 3784–3788.
ICPRICPR-2010-MemonLM #modelling
Information Theoretic Expectation Maximization Based Gaussian Mixture Modeling for Speaker Verification (SM, ML, NCM), pp. 4536–4540.
ICPRICPR-2010-PuS #learning #probability
Probabilistic Measure for Signature Verification Based on Bayesian Learning (DP, SNS), pp. 1188–1191.
ICPRICPR-2010-VillegasP #video
Fusion of Qualities for Frame Selection in Video Face Verification (MV, RP), pp. 1302–1305.
ICPRICPR-2010-WilliamsTSB #analysis #multi
Body Motion Analysis for Multi-modal Identity Verification (GW, GWT, KS, CB), pp. 2198–2201.
ICPRICPR-2010-ZafrullaBYPSH #education #game studies
American Sign Language Phrase Verification in an Educational Game for Deaf Children (ZZ, HB, PY, PP, TS, HH), pp. 3846–3849.
KEODKEOD-2010-AnjumHY #ontology
Cross Domain Knowledge Verification — Verifying Knowledge in Foundation Ontology based Domain Ontologies (NAA, JAH, BY), pp. 339–342.
KEODKEOD-2010-KezadriP #ontology #towards #validation
First Steps Toward a Verification and Validation Ontology (MK, MP), pp. 440–444.
KMISKMIS-2010-LodemannL #framework #ontology
Ontology-based Railway Infrastructure Verification — Planning Benefits (ML, NL), pp. 176–181.
SEKESEKE-2010-BernhartAMG #automation #case study #experience #framework #integration #testing
Automated Integration Testing and Verification of a Secured SOA Infrastructure — an Experience Report in eHealth (MB, TA, AM, TG), pp. 198–202.
SEKESEKE-2010-BinGHMMPRST #hardware #ontology #tool support
Ontology-Based Tools in the Service of Hardware Verification (EB, AG, KH, EM, RM, OP, MR, GS, ET), pp. 303–308.
SEKESEKE-2010-GoelXS #multi #network #online
A Multi-State Bayesian Network for Shill Verification in Online Auctions (AG, HX, SMS), pp. 279–285.
SEKESEKE-2010-ParkHK #diagrams #sequence chart #uml
Formal Verification of UML 2.0 Sequence Diagram (SP, TH, GK), pp. 411–416.
SIGIRSIGIR-2010-Roussinov #aspect-oriented
Aspect presence verification conditional on other aspects (DR), pp. 865–866.
MODELSMoDELS-v1-2010-RahimW #code generation #consistency #semantics #state machine
Verifying Semantic Conformance of State Machine-to-Java Code Generators (LAR, JW), pp. 166–180.
ECOOPECOOP-2010-StadenCM #execution #logic #object-oriented #specification
Verifying Executable Object-Oriented Specifications with Separation Logic (SvS, CC, BM), pp. 151–174.
ECOOPECOOP-2010-SvendsenBP
Verifying Generics and Delegates (KS, LB, MJP), pp. 175–199.
AdaEuropeAdaEurope-2010-BritoP #case study #comparative
Program Verification in SPARK and ACSL: A Comparative Case Study (EB, JSP), pp. 97–110.
LOPSTRLOPSTR-2010-FioravantiPPS #evaluation #infinity
Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation (FF, AP, MP, VS), pp. 164–183.
LOPSTRLOPSTR-2010-GiorginoSMP #algorithm #graph
Verification of the Schorr-Waite Algorithm — From Trees to Graphs (MG, MS, RM, MP), pp. 67–83.
PLDIPLDI-2010-ChenCS #compilation #security
Type-preserving compilation of end-to-end verification of security enforcement (JC, RC, NS), pp. 412–423.
PLDIPLDI-2010-EmmiMM #transaction
Parameterized verification of transactional memories (ME, RM, RM), pp. 134–145.
PLDIPLDI-2010-YangH #automation #operating system #type safety
Safe to the last instruction: automated verification of a type-safe operating system (JY, CH), pp. 99–110.
POPLPOPL-2010-AtigBBM #memory management #modelling #on the #problem
On the verification problem for weak memory models (MFA, AB, SB, MM), pp. 7–18.
POPLPOPL-2010-AttiyaRR
Sequential verification of serializability (HA, GR, NR), pp. 31–42.
POPLPOPL-2010-BhargavanFG #composition #protocol #security #type system
Modular verification of security protocol code by typing (KB, CF, ADG), pp. 445–456.
POPLPOPL-2010-KobayashiTU #higher-order #multi #recursion #transducer
Higher-order multi-parameter tree transducers and recursion schemes for program verification (NK, NT, HU), pp. 495–508.
POPLPOPL-2010-NanevskiVB #source code
Structuring the verification of heap-manipulating programs (AN, VV, JB), pp. 261–274.
POPLPOPL-2010-SrivastavaGF #synthesis
From program verification to program synthesis (SS, SG, JSF), pp. 313–326.
PPDPPPDP-2010-JacquemardR #xml
Rewrite-based verification of XML updates (FJ, MR), pp. 119–130.
QAPLQAPL-2010-BarsottiW #abstraction #automation #probability #random
Automatic Probabilistic Program Verification through Random Variable Abstraction (DB, NW), pp. 34–47.
SASSAS-2010-Fahndrich #contract
Static Verification for Code Contracts (MF), pp. 2–5.
SASSAS-2010-HofmannKS #coq
Verifying a Local Generic Solver in Coq (MH, AK, HS), pp. 340–355.
SASSAS-2010-VechevYRS #automation #parallel #source code
Automatic Verification of Determinism for Structured Parallel Programs (MTV, EY, RR, VS), pp. 455–471.
REFSQREFSQ-2010-SabaliauskaiteLEURRGF #challenge #industrial #requirements #scalability
Challenges in Aligning Requirements Engineering and Verification in a Large-Scale Industrial Context (GS, AL, EE, MU, BR, PR, TG, RF), pp. 128–142.
ASEASE-2010-BorgesGL #adaptation #self
Integrating model verification and self-adaptation (RVB, ASdG, LCL), pp. 317–320.
FSEFSE-2010-LiG #gpu #kernel #scalability #smt
Scalable SMT-based verification of GPU kernel functions (GL, GG), pp. 187–196.
ICSEICSE-2010-ClassenHSLR #model checking #performance #product line
Model checking lots of systems: efficient verification of temporal properties in software product lines (AC, PH, PYS, AL, JFR), pp. 335–344.
ICSEICSE-2010-Elmas #abstraction #concurrent #named #proving #reduction
QED: a proof system based on reduction and abstraction for the static verification of concurrent software (TE), pp. 507–508.
ICSEICSE-2010-YangL #approach #bound
A cut-off approach for bounded verification of parameterized systems (QY, ML), pp. 345–354.
SACSAC-2010-CiraciBA #constraints #graph
Graph-based verification of static program constraints (SC, PvdB, MA), pp. 2265–2272.
SACSAC-2010-GehlertBKMPP #adaptation
Exploiting assumption-based verification for the adaptation of service-based applications (AG, AB, RK, AM, MP, KP), pp. 2430–2437.
SACSAC-2010-HurnausP #automation #composition #contract #programming
Programming assistance based on contracts and modular verification in the automation domain (DH, HP), pp. 2544–2551.
SACSAC-2010-IqbalKFD #email #forensics
e-mail authorship verification for forensic investigation (FI, LAK, BCMF, MD), pp. 1591–1598.
SACSAC-2010-KokashKV #composition #design
Data-aware design and verification of service compositions with Reo and mCRL2 (NK, CK, EPdV), pp. 2406–2413.
SACSAC-2010-RoyM #visual notation
Visual processing-inspired fern-audio features for noise-robust speaker verification (AR, SM), pp. 1491–1495.
SACSAC-2010-VogelsJP #generative #performance #proving
A machine-checked soundness proof for an efficient verification condition generator (FV, BJ, FP), pp. 2517–2522.
LDTALDTA-J-2007-CamachoMBV #automation #generative #tool support #using
Automated generation of program translation and verification tools using annotated grammars (DOC, KM, MvdB, JJV), pp. 3–20.
LDTALDTA-2010-CruzHP #analysis #named #online
GamaSlicer: an online laboratory for program verification and analysis (DCdC, PRH, JSP), p. 3.
ASPLOSASPLOS-2010-RomanescuLS #consistency #memory management #specification
Specifying and dynamically verifying address translation-aware memory consistency (BFR, ARL, DJS), pp. 323–334.
CCCC-2010-BurckhardtMS #memory management #modelling
Verifying Local Transformations on Relaxed Memory Models (SB, MM, VS), pp. 104–123.
DACDAC-2010-Coudert #algorithm #performance
An efficient algorithm to verify generalized false paths (OC), pp. 188–193.
DACDAC-2010-HazraMDPBG #architecture #modelling
Leveraging UPF-extracted assertions for modeling and formal verification of architectural power intent (AH, SM, PD, AP, DB, KG), pp. 773–776.
DACDAC-2010-KundertC #functional #modelling
Model-based functional verification (KSK, HC), pp. 421–424.
DACDAC-2010-LiFS #mining #scalability #specification
Scalable specification mining for verification and diagnosis (WL, AF, SAS), pp. 755–760.
DACDAC-2010-NahirZGHACBFBK #validation
Bridging pre-silicon verification and post-silicon validation (AN, AZ, RG, AJH, MA, AC, BB, HF, VB, SK), pp. 94–95.
DACDAC-2010-ThomptoH #fault tolerance
Verification for fault tolerance of the IBM system z microprocessor (BWT, BH), pp. 525–530.
DACDAC-2010-XiongW #algorithm #constraints #grid #linear #performance #power management
An efficient dual algorithm for vectorless power grid verification under linear current constraints (XX, JW), pp. 837–842.
DATEDATE-2010-BraunBLR #interface #specification
Simulation-based verification of the MOST NetInterface specification revision 3.0 (AB, OB, DL, WR), pp. 538–543.
DATEDATE-2010-FerroP #modelling #semantics #transaction
Formal semantics for PSL modeling layer and application to the verification of transactional models (LF, LP), pp. 1207–1212.
DATEDATE-2010-LammermannRKRVJH #design #towards
Towards assertion-based verification of heterogeneous system designs (SL, JR, TK, WR, AV, AJ, LH), pp. 1171–1176.
DATEDATE-2010-NarayananAZTP #process
Formal verification of analog circuits in the presence of noise and process variation (RN, BA, MHZ, ST, LCP), pp. 1309–1312.
DATEDATE-2010-OliveiraZ0
Assertion-based verification of RTOS properties (MFdSO, HZ, WM), pp. 630–633.
DATEDATE-2010-SoekenWKGD #modelling #ocl #satisfiability #uml #using
Verifying UML/OCL models using Boolean satisfiability (MS, RW, MK, MG, RD), pp. 1341–1344.
DATEDATE-2010-ZhangLL #approach #markov #modelling #simulation #using
An abstraction-guided simulation approach using Markov models for microprocessor verification (TZ, TL, XL), pp. 484–489.
HPDCHPDC-2010-GehaniK #multi #named #trust
Mendel: efficiently verifying the lineage of data modified in multiple trust domains (AG, MK), pp. 227–239.
PPoPPPPoPP-2010-LiGKQ #source code
A symbolic verifier for CUDA programs (GL, GG, RMK, DQ), pp. 357–358.
ESOPESOP-2010-AmtoftHR #array #automation #certification #contract #data flow #precise #reasoning #source code
Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays (TA, JH, ER), pp. 43–63.
ESOPESOP-2010-BlazyRA #graph
Formal Verification of Coalescing Graph-Coloring Register Allocation (SB, BR, AWA), pp. 145–164.
ESOPESOP-2010-Lochbihler #compilation #java #thread
Verifying a Compiler for Java Threads (AL), pp. 427–447.
FASEFASE-2010-EhrigERBP #analysis #formal method #self
Formal Analysis and Verification of Self-Healing Systems (HE, CE, OR, AB, PP), pp. 139–153.
TACASTACAS-2010-KatzP #automation
Code Mutation in Verification and Automatic Code Correction (GK, DP), pp. 435–450.
TACASTACAS-2010-KwiatkowskaNPQ #probability
Assume-Guarantee Verification for Probabilistic Systems (MZK, GN, DP, HQ), pp. 23–37.
TACASTACAS-2010-LeinoR #design #encoding #logic #polymorphism
A Polymorphic Intermediate Verification Language: Design and Logical Encoding (KRML, PR), pp. 312–327.
CAVCAV-2010-BallBLKL #framework #platform #research
The Static Driver Verifier Research Platform (TB, EB, VL, RK, JL), pp. 119–122.
CAVCAV-2010-BraytonM #named
ABC: An Academic Industrial-Strength Verification Tool (RKB, AM), pp. 24–40.
CAVCAV-2010-CohenMST #concurrent #invariant #source code
Local Verification of Global Invariants in Concurrent Programs (EC, MM, WS, ST), pp. 480–494.
CAVCAV-2010-CohenNS10a #composition #ltl #named
SPLIT: A Compositional LTL Verifier (AC, KSN, YS), pp. 558–561.
CAVCAV-2010-ConwayB #data type #implementation #low level
Verifying Low-Level Implementations of High-Level Datatypes (CLC, CB), pp. 306–320.
CAVCAV-2010-Donze #hybrid #parametricity #synthesis
Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems (AD), pp. 167–170.
CAVCAV-2010-KawaguchiRJ #named #safety
Dsolve: Safety Verification via Liquid Types (MK, PMR, RJ), pp. 123–126.
CAVCAV-2010-McMillan #lazy evaluation #testing
Lazy Annotation for Program Testing and Verification (KLM), pp. 104–118.
CAVCAV-2010-PnueliSZ #algorithm #framework #named
Jtlv: A Framework for Developing Verification Algorithms (AP, YS, LDZ), pp. 171–174.
CAVCAV-2010-PulinaT #abstraction #approach #network
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks (LP, AT), pp. 243–257.
CAVCAV-2010-RepsLTBL
There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code (TWR, JL, AVT, GB, AL), pp. 41–56.
CAVCAV-2010-Rybalchenko #constraints #theorem proving #theory and practice
Constraint Solving for Program Verification: Theory and Practice by Example (AR), pp. 57–71.
CAVCAV-2010-ZhangSRHH #hybrid #probability #safety
Safety Verification for Probabilistic Hybrid Systems (LZ, ZS, SR, HH, EMH), pp. 196–211.
CSLCSL-2010-Rybalchenko #constraints #theorem proving #theory and practice
Constraint Solving for Program Verification: Theory and Practice by Example (AR), p. 51.
ICLPICLP-2010-Lopez-GarciaDB10 #debugging #framework #resource management
A Framework for Verification and Debugging of Resource Usage Properties: Resource Usage Verification (PLG, LD, FB), pp. 104–113.
ICSTICST-2010-AsztalosLL #automation #model transformation #towards
Towards Automated, Formal Verification of Model Transformations (MA, LL, TL), pp. 15–24.
ICSTICST-2010-FeldtTAR #challenge #industrial #process #validation
Challenges with Software Verification and Validation Activities in the Space Industry (RF, RT, EA, BR), pp. 225–234.
ICSTICST-2010-Laurent #concept #formal method #process #testing #using #validation
Using Formal Methods and Testability Concepts in the Avionics Systems Validation and Verification (V&V) Process (OL), pp. 1–10.
IJCARIJCAR-2010-AyadM #float #multi #source code
Multi-Prover Verification of Floating-Point Programs (AA, CM), pp. 127–141.
IJCARIJCAR-2010-ChaudhuriDLM #proving #safety
Verifying Safety Properties with the TLA+ Proof System (KC, DD, LL, SM), pp. 142–148.
IJCARIJCAR-2010-Sofronie-Stokkermans #parametricity #reasoning
Hierarchical Reasoning for the Verification of Parametric Systems (VSS), pp. 171–187.
ISSTAISSTA-2010-GaleottiRPF #analysis #bound #invariant #performance
Analysis of invariants for efficient bounded verification (JPG, NR, CLP, MFF), pp. 25–36.
LICSLICS-2010-Moore #proving #theorem proving
Theorem Proving for Verification: The Early Days (JSM), p. 283.
TAPTAP-2010-AhnD #axiom #first-order #logic #testing
Testing First-Order Logic Axioms in Program Verification (KYA, ED), pp. 22–37.
TAPTAP-2010-GladischTBY #generative #testing #using
Generating Regression Unit Tests Using a Combination of Verification and Capture & Replay (CG, SST, BB, AY), pp. 61–76.
VMCAIVMCAI-2010-BuZL #automaton #hybrid #programming #reachability #using
Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming (LB, JZ, XL), pp. 78–94.
VMCAIVMCAI-2010-ChadhaLPV #bound #complexity #realtime
Complexity Bounds for the Verification of Real-Time Software (RC, AL, PP, MV), pp. 95–111.
VMCAIVMCAI-2010-Leino #concurrent #source code
Verifying Concurrent Programs with Chalice (KRML), p. 2.
WICSA-ECSAWICSA-ECSA-2009-BritoRL #architecture #fault tolerance
Verifying architectural variabilities in software fault tolerance techniques (PHSB, CMFR, RdL), pp. 231–240.
WICSA-ECSAWICSA-ECSA-2009-BucchiaronePVR #modelling #self #using
Self-Repairing systems modeling and verification using AGG (AB, PP, CV, OR), pp. 181–190.
DocEngDocEng-2009-SchonbergWJF #documentation
Logic-based verification of technical documentation (CS, FW, MJ, BF), pp. 251–252.
DRRDRR-2009-LiD #difference #independence #using
Improving semi-text-independent method of writer verification using difference vector (XL, XD), pp. 1–10.
DRRDRR-2009-SrihariB #comparison #modelling #statistics
Comparison of statistical models for writer verification (SNS, GRB), pp. 1–10.
ICDARICDAR-2009-Alonso-FernandezFGGO #robust
Robustness of Signature Verification Systems to Imitators with Increasing Skills (FAF, JF, AG, JG, JOG), pp. 728–732.
ICDARICDAR-2009-BatistaGS #approach #multi
A Multi-Hypothesis Approach for Off-Line Signature Verification with HMMs (LB, EG, RS), pp. 1315–1319.
ICDARICDAR-2009-BlankersHFV #contest
ICDAR 2009 Signature Verification Competition (VLB, CEvdH, KF, LV), pp. 1403–1407.
ICDARICDAR-2009-BonillaFGH #pseudo
Offline Signature Verification Based on Pseudo-Cepstral Coefficients (JFVB, MAFB, CMTG, JBAH), pp. 126–130.
ICDARICDAR-2009-GalballyFMO #evaluation #using
Evaluation of Brute-force Attack to Dynamic Signature Verification Using Synthetic Samples (JG, JF, MMD, JOG), pp. 131–135.
ICDARICDAR-2009-IbrahimKKAG #analysis #dependence #online #using
On-Line Signature Verification: Directional Analysis of a Signature Using Weighted Relative Angle Partitions for Exploitation of Inter-Feature Dependencies (MTI, MJK, MAK, KSA, LG), pp. 41–45.
ICDARICDAR-2009-NguyenBL #problem
Global Features for the Off-Line Signature Verification Problem (VN, MB, GL), pp. 1300–1304.
ICDARICDAR-2009-PrakashG #geometry
Geometric Centroids and their Relative Distances for Off-line Signature Verification (HNP, DSG), pp. 121–125.
ICDARICDAR-2009-WangHL
A New Block Partitioned Text Feature for Text Verification (XW, LH, CL), pp. 366–370.
VLDBVLDB-2009-PangZM #database #outsourcing #scalability
Scalable Verification for Outsourced Dynamic Databases (HP, JZ, KM), pp. 802–813.
CSMRCSMR-2009-KellensSDJP #cobol #design #framework #named
Cognac: A Framework for Documenting and Verifying the Design of Cobol Systems (AK, KDS, TD, LJ, BVP), pp. 199–208.
CIAACIAA-2009-AtigT #communication #parallel #source code
Verifying Parallel Programs with Dynamic Communication Structures (MFA, TT), pp. 145–154.
ICALPICALP-v2-2009-Boldo #case study #float
Floats and Ropes: A Case Study for Formal Numerical Program Verification (SB), pp. 91–102.
LATALATA-2009-JiraskovaP #automaton #self
Converting Self-verifying Automata into Deterministic Automata (GJ, GP), pp. 458–468.
FMFM-2009-AlpuenteBR #logic #specification #web
Specification and Verification of Web Applications in Rewriting Logic (MA, DB, DR), pp. 790–805.
FMFM-2009-HarrisKCJR #bound #data flow #process
Verifying Information Flow Control over Unbounded Processes (WRH, NK, SC, SJ, TWR), pp. 773–789.
FMFM-2009-LarsenLNP #realtime #requirements
Verifying Real-Time Systems against Scenario-Based Requirements (KGL, SL, BN, SP), pp. 676–691.
FMFM-2009-LeinenbachS
Verifying the Microsoft Hyper-V Hypervisor with VCC (DL, TS), pp. 806–809.
FMFM-2009-LeuschelFFP #automation #modelling #scalability
Automated Property Verification for Large Scale B Models (ML, JF, FF, DP), pp. 708–723.
FMFM-2009-LuthW #c #source code #specification
Certifiable Specification and Verification of C Programs (CL, DW), pp. 419–434.
FMFM-2009-OHalloran
Guess and Verify — Back to the Future (CO), pp. 23–32.
FMFM-2009-PlatzerC #case study
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study (AP, EMC), pp. 547–562.
FMFM-2009-Rajamani #statistics #testing
Verification, Testing and Statistics (SKR), pp. 33–40.
FMFM-2009-SouyrisWDD
Formal Verification of Avionics Software Products (JS, VW, DD, HD), pp. 532–546.
IFMIFM-2009-BuiN #random
Formal Verification Based on Guided Random Walks (THB, AN), pp. 72–87.
IFMIFM-2009-CabotCR #contract #ocl #uml
Verifying UML/OCL Operation Contracts (JC, RC, DR), pp. 40–55.
IFMIFM-2009-LangariT #graph transformation
Application of Graph Transformation in Verification of Dynamic Systems (ZL, RJT), pp. 261–276.
SEFMSEFM-2009-BersaniFPR #modelling #multi #paradigm #realtime
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms (MMB, CAF, MP, MR), pp. 13–22.
SEFMSEFM-2009-Chalin
Adjusted Verification Rules for Loops Are More Complete and Give Better Diagnostics for Less (PC), pp. 317–324.
SEFMSEFM-2009-EzekielL #approach #automation #multi
An Automated Approach to Verifying Diagnosability in Multi-agent Systems (JE, AL), pp. 51–60.
SEFMSEFM-2009-Jeannet #concurrent #interprocedural #relational #source code
Relational Interprocedural Verification of Concurrent Programs (BJ), pp. 83–92.
SEFMSEFM-2009-Rushby #assurance
Software Verification and System Assurance (JMR), pp. 3–10.
SEFMSEFM-2009-TatsutaCA #logic #pointer
Completeness of Pointer Program Verification by Separation Logic (MT, WNC, MFAA), pp. 179–188.
ICFPICFP-2009-KleinDE #case study #experience #kernel
Experience report: seL4: formally verifying a high-performance microkernel (GK, PD, KE), pp. 91–96.
CAiSECAiSE-2009-LiuLYWH #analysis #constraints #using #workflow
ETL Workflow Analysis and Verification Using Backwards Constraint Propagation (JL, SL, DY, JW, TH), pp. 455–469.
CAiSECAiSE-2009-PlanasCG #action semantics #behaviour #modelling #semantics #specification #uml
Verifying Action Semantics Specifications in UML Behavioral Models (EP, JC, CG), pp. 125–140.
EDOCEDOC-2009-BoukhebouzeABM #modelling #process #rule-based #using
Rule-Based Modeling and Verification of Business Processes Using ECAPE Net (MB, YA, ANB, ZM), p. 74–?.
ICEISICEIS-HCI-2009-NakanishiTO #artificial reality #complexity #design #effectiveness #guidelines #using
Study for Establishing Design Guidelines for Manuals using Augmented Reality Technology — Verification and Expansion of the Basic Model Describing “Effective Complexity” (MN, SiT, YO), pp. 21–26.
ICEISICEIS-J-2009-MoralesC #automation #composition #process
Automatic Compositional Verification of Business Processes (LEMM, MIC), pp. 479–490.
SEKESEKE-2009-ShahrokniFPB #challenge #robust
Robustness Verification Challenges in Automotive Telematics Software (AS, RF, FP, AB), pp. 460–465.
SEKESEKE-2009-YuanHZL #automation #modelling #multi #transaction
Modeling and Verification of Automatic Multi-business Transactions (MY, ZH, JZ, XL), pp. 274–279.
SEKESEKE-2009-ZhangLSDCL #scalability
Formal Verification of Scalable NonZero Indicators (SJZ, YL, JS, JSD, WC, YAL), pp. 406–411.
MODELSMoDELS-2009-KraemerH #automation #development #encapsulation #incremental #process #uml
Automated Encapsulation of UML Activities for Incremental Development and Verification (FAK, PH), pp. 571–585.
SPLCSPLC-2009-GanesanLAMB #architecture #design #product line
Verifying architectural design rules of the flight software product line (DG, ML, CA, DM, MB), pp. 161–170.
MODELSMoDELS-2009-KraemerH #automation #development #encapsulation #incremental #process #uml
Automated Encapsulation of UML Activities for Incremental Development and Verification (FAK, PH), pp. 571–585.
AdaEuropeAdaEurope-2009-BerthomieuBCDFV #specification
Formal Verification of AADL Specifications in the Topcased Environment (BB, JPB, CC, SDZ, MF, FV), pp. 207–221.
PADLPADL-2009-WangBLS #declarative #network
Declarative Network Verification (AW, PB, BTL, OS), pp. 61–75.
PLDIPLDI-2009-KawaguchiRJ #data type #type system
Type-based data structure verification (MK, PMR, RJ), pp. 304–315.
PLDIPLDI-2009-SrivastavaG #abstraction #using
Program verification using templates over predicate abstraction (SS, SG), pp. 223–234.
POPLPOPL-2009-GantyMR #liveness #source code
Verifying liveness for asynchronous programs (PG, RM, AR), pp. 102–113.
POPLPOPL-2009-HawblitzelP #automation #garbage collection
Automated verification of practical garbage collectors (CH, EP), pp. 441–453.
POPLPOPL-2009-Kobayashi #higher-order #recursion #source code
Types and higher-order recursion schemes for verification of higher-order programs (NK), pp. 416–428.
POPLPOPL-2009-Ridge #approach #distributed
Verifying distributed systems: the operational approach (TR), pp. 429–440.
PPDPPPDP-2009-Virseda #algorithm #debugging #declarative #framework #higher-order #logic #source code
A higher-order logical framework for the algorithmic debugging and verification of declarative programs (RdVV), pp. 49–60.
SASSAS-2009-Qadeer #algorithm #smt #using
Algorithmic Verification of Systems Software Using SMT Solvers (SQ), p. 2.
AdaSIGAda-2009-Knight #ada #approach #named
Echo: a new approach to formal verification based on Ada (JK), pp. 85–86.
RERE-2009-Hall #forensics
Forensic System Verification (RJH), pp. 111–120.
RERE-2009-PostSMGK #functional #requirements
Linking Functional Requirements and Software Verification (HP, CS, FM, TG, TK), pp. 295–302.
RERE-2009-SalinesiRDM #classification #fault #feature model #modelling #product line #towards
Looking for Product Line Feature Models Defects: Towards a Systematic Classification of Verification Criteria (CS, CR, DD, RM), pp. 385–386.
ASEASE-2009-Jenson #component #constraints #dependence #validation
Improving Component Dependency Resolution with Soft Constraints, Validation and Verification (GJ), pp. 716–720.
ASEASE-2009-RayMACSM #using #validation
Validating Automotive Control Software Using Instrumentation-Based Verification (AR, IM, CA, RC, CPS, CM), pp. 15–25.
ESEC-FSEESEC-FSE-2009-BozzanoCRKNN #evaluation #modelling #performance
Verification and performance evaluation of aadl models (MB, AC, MR, JPK, VYN, TN), pp. 285–286.
ESEC-FSEESEC-FSE-2009-HannaBR #automation #automaton #behaviour #composition #independence
Behavioral automata composition for automatic topology independent verification of parameterized systems (YH, SB, HR), pp. 325–334.
SACSAC-2009-BaechlerBH #image #modelling #using
Labeled images verification using Gaussian mixture models (MB, JLB, JH), pp. 1331–1335.
SACSAC-2009-BeekMG #framework #named
CMC-UMC: a framework for the verification of abstract service-oriented properties (MHtB, FM, SG), pp. 2111–2117.
SACSAC-2009-GiroD #automaton #on the #probability
On the verification of probabilistic I/O automata with unspecified rates (SG, PRD), pp. 582–586.
SACSAC-2009-RodriguesSC #composition #embedded #functional #set #using
Improving functional verification of embedded systems using hierarchical composition and set theory (CLR, KRGdS, HdNC), pp. 1632–1636.
SACSAC-2009-SharyginaTT #abstraction #performance #precise
The synergy of precise and fast abstractions for program verification (NS, ST, AT), pp. 566–573.
SACSAC-2009-SongKS #approach #aspect-oriented #modelling
A property-based verification approach in aspect-oriented modeling (ES, HK, WS), pp. 545–546.
CASECASE-2009-AlenljungL #graph #using
Formal verification of PLC controlled systems using Sensor Graphs (TA, BL), pp. 164–170.
CASECASE-2009-AllenGT #logic #nondeterminism
Closed-loop determinism for non-deterministic environments: Verification for IEC 61499 logic controllers (LVA, KMG, DMT), pp. 1–6.
CASECASE-2009-VoronovA #model checking #process #using
Verification of process operations using model checking (AV, ), pp. 415–420.
DACDAC-2009-AlimohammadFC
FPGA-based accelerator for the verification of leading-edge wireless systems (AA, SFF, BFC), pp. 844–847.
DACDAC-2009-Chesters #development #lifecycle
Role of the verification team throughout the ASIC development life cycle (EC), pp. 216–219.
DACDAC-2009-GhaniN #approximate #grid #performance #power management #using
Fast vectorless power grid verification using an approximate inverse technique (NHAG, FNN), pp. 184–189.
DACDAC-2009-GluskaL #modelling
Shortening the verification cycle with synthesizable abstract models (AG, LL), pp. 454–459.
DACDAC-2009-GodlinS
Regression verification (BG, OS), pp. 466–471.
DACDAC-2009-MarcilioSAR #behaviour #novel
A novel verification technique to uncover out-of-order DUV behaviors (GM, LCVdS, BA, SR), pp. 448–453.
DACDAC-2009-RanjanCS #debugging
Beyond verification: leveraging formal for debugging (RKR, CC, SS), pp. 648–651.
DACDAC-2009-StapletonT #component #design #problem #reuse
Verification problems in reusing internal design components (WS, PT), pp. 209–211.
DACDAC-2009-Thaker #question
Holistic verification: myth or magic bullet? (PAT), pp. 204–208.
DACDAC-2009-Whipp #architecture #process
Exploiting “architecture for verification” to streamline the verification process (DW), pp. 212–215.
DATEDATE-2009-AlimohammadFC #algorithm #architecture #development #flexibility
A flexible layered architecture for accurate digital baseband algorithm development and verification (AA, SFF, BFC), pp. 45–50.
DATEDATE-2009-BarkeGGHHPSW #formal method
Formal approaches to analog circuit verification (EB, DG, HG, LH, SH, RP, SS, YW), pp. 724–729.
DATEDATE-2009-BombieriFPHL #functional
Functional qualification of TLM verification (NB, FF, GP, MH, FL), pp. 190–195.
DATEDATE-2009-CabodiCGMNQ #constraints #model checking
Speeding up model checking by exploiting explicit and hidden verification constraints (GC, PC, LG, MM, SN, SQ), pp. 1686–1691.
DATEDATE-2009-HeH #algorithm #encoding #performance
An efficient path-oriented bitvector encoding width computation algorithm for bit-precise verification (NH, MSH), pp. 1602–1607.
DATEDATE-2009-LettninNBRGKRSR #hardware
Semiformal verification of temporal properties in automotive hardware dependent software (DL, PKN, JB, JR, JG, TK, WR, VS, SR), pp. 1214–1217.
DATEDATE-2009-RichterJE #framework #learning
Learning early-stage platform dimensioning from late-stage timing verification (KR, MJ, RE), pp. 851–857.
HPCAHPCA-2009-ChenLHCSWP #consistency #memory management #performance
Fast complete memory consistency verification (YC, YL, WH, TC, HS, PW, HP), pp. 381–392.
LCTESLCTES-2009-AndreM #requirements #specification
Specification and verification of time requirements with CCSL and Esterel (CA, FM), pp. 167–176.
PDPPDP-2009-HermannsGWW #performance #scalability
Verifying Causality between Distant Performance Phenomena in Large-Scale MPI Applications (MAH, MG, FW, BJNW), pp. 78–84.
PPoPPPPoPP-2009-VoVDGKT #source code
Formal verification of practical MPI programs (AV, SSV, MD, GG, RMK, RT), pp. 261–270.
SOSPSOSP-2009-KleinEHACDEEKNSTW #kernel #named
seL4: formal verification of an OS kernel (GK, KE, GH, JA, DC, PD, DE, KE, RK, MN, TS, HT, SW), pp. 207–220.
ESOPESOP-2009-KikuchiK #authentication #automation #encryption #protocol #type system
Type-Based Automated Verification of Authenticity in Cryptographic Protocols (DK, NK), pp. 222–236.
ESOPESOP-2009-LeinoM #concurrent #multi #source code #thread
A Basis for Verifying Multi-threaded Programs (KRML, PM), pp. 378–393.
ESOPESOP-2009-RajanTSL #composition #design #named #policy #web #web service
Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services (HR, JT, SMS, GTL), pp. 333–347.
ESOPESOP-2009-SchaferEM #attribute grammar #coq #formal method
Formalising and Verifying Reference Attribute Grammars in Coq (MS, TE, OdM), pp. 143–159.
FASEFASE-2009-BoronatHM #logic #model transformation #semantics
Rewriting Logic Semantics and Verification of Model Transformations (AB, RH, JM), pp. 18–33.
FASEFASE-2009-GiannakopoulouP #composition #generative #interface
Interface Generation and Compositional Verification in JavaPathfinder (DG, CSP), pp. 94–108.
FASEFASE-2009-Sery #specification
Enhanced Property Specification and Verification in BLAST (OS), pp. 456–469.
TACASTACAS-2009-BrughNR #dot-net #named #source code
MoonWalker: Verification of .NET Programs (NHMAdB, VYN, TCR), pp. 170–173.
TACASTACAS-2009-ChenFCTW #automaton #composition #learning
Learning Minimal Separating DFA’s for Compositional Verification (YFC, AF, EMC, YKT, BYW), pp. 31–45.
TACASTACAS-2009-EmmiJKM #implementation
Verifying Reference Counting Implementations (ME, RJ, EK, RM), pp. 352–367.
TACASTACAS-2009-YuBI #analysis #string
Symbolic String Verification: Combining String Analysis and Size Analysis (FY, TB, OHI), pp. 322–336.
CADECADE-2009-PlatzerQR
Real World Verification (AP, JDQ, PR), pp. 485–501.
CAVCAV-2009-BensalemBNS #composition #concurrent #detection #named
D-Finder: A Tool for Compositional Deadlock Detection and Verification (SB, MB, THN, JS), pp. 614–619.
CAVCAV-2009-BozgaHIKV #array #automation #integer #source code
Automatic Verification of Integer Array Programs (MB, PH, RI, FK, TV), pp. 157–172.
CAVCAV-2009-HuntS
Centaur Technology Media Unit Verification (WAHJ, SS), pp. 353–367.
CAVCAV-2009-KaivolaGNTWPSTFRN #execution #testing #validation
Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation (RK, RG, NN, AT, JW, SP, AS, CT, VF, ER, AN), pp. 414–429.
CAVCAV-2009-Kim #performance
Mixed-Signal System Verification: A High-Speed Link Example (JK), p. 16.
CAVCAV-2009-LomuscioQR #model checking #multi #named
MCMAS: A Model Checker for the Verification of Multi-Agent Systems (AL, HQ, FR), pp. 682–688.
CAVCAV-2009-SrivastavaGF #named #smt
VS3: SMT Solvers for Program Verification (SS, SG, JSF), pp. 702–708.
CAVCAV-2009-Strichman #equivalence #proving #source code
Regression Verification: Proving the Equivalence of Similar Programs (OS), p. 63.
CAVCAV-2009-SunLDP #flexibility #named #towards
PAT: Towards Flexible Verification under Fairness (JS, YL, JSD, JP), pp. 709–714.
ICLPICLP-2009-MeraLH #framework #runtime #testing
Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework (EM, PLG, MVH), pp. 281–295.
LICSLICS-2009-GollerMT #complexity #on the #process
On the Computational Complexity of Verifying One-Counter Processes (SG, RM, AWT), pp. 235–244.
TAPTAP-2009-NoriR #statistics #testing
Verification, Testing and Statistics (AVN, SKR), pp. 6–9.
VMCAIVMCAI-2009-Cortier #protocol #security
Verification of Security Protocols (VC), pp. 5–13.
VMCAIVMCAI-2009-Vafeiadis #abstraction
Shape-Value Abstraction for Verifying Linearizability (VV), pp. 335–348.
CBSECBSE-2008-ChoiB #component #design #towards
Towards Component-Based Design and Verification of a µ-Controller (YC, CB), pp. 196–211.
ECSAECSA-2008-Atkinson #architecture #component #testing
Component-Oriented Verification of Software Architectures through Built-in Tests (CA), p. 2.
DRRDRR-2008-BrinkKS #automation #identification
Automatic removal of crossed-out handwritten text and the effect on writer verification and identification (AB, HvdK, LS), p. 68150.
VLDBVLDB-2008-ShangZLY #algorithm #morphism #performance #testing
Taming verification hardness: an efficient algorithm for testing subgraph isomorphism (HS, YZ, XL, JXY), pp. 364–375.
CSMRCSMR-2008-LiTLMC #requirements #validation
Coping with Requirements Changes in Software Verification and Validation (SL, LT, WL, MM, GC), pp. 317–318.
ICALPICALP-B-2008-BrazdilFK #branch #markov #process #synthesis
Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives (TB, VF, AK), pp. 148–159.
ICALPICALP-C-2008-HallgrenKSZ #protocol #quantum
Making Classical Honest Verifier Zero Knowledge Protocols Secure against Quantum Attacks (SH, AK, PS, SZ), pp. 592–603.
FMFM-2008-ArvindDK #design
Getting Formal Verification into Design Flow (A, ND, MK), pp. 12–32.
FMFM-2008-EmmiGP #automaton #interface
Assume-Guarantee Verification for Interface Automata (ME, DG, CSP), pp. 116–131.
FMFM-2008-FuriaPR #approximate #automation #specification
Automated Verification of Dense-Time MTL Specifications Via Discrete-Time Approximation (CAF, MP, MR), pp. 132–147.
FMFM-2008-GrandyBSSR #protocol #security
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
Verifying Dynamic Pointer-Manipulating Threads (TN, SR), pp. 84–99.
SEFMSEFM-2008-BartheKPS #hybrid #proving
Preservation of Proof Pbligations for Hybrid Verification Methods (GB, CK, DP, JSF), pp. 127–136.
SEFMSEFM-2008-QuintonG #component #contract
Contract-Based Verification of Hierarchical Systems of Components (SQ, SG), pp. 377–381.
SEFMSEFM-2008-SchaeferP #adaptation #composition #embedded #modelling #reasoning
Compositional Reasoning in Model-Based Verification of Adaptive Embedded Systems (IS, APH), pp. 95–104.
SEFMSEFM-2008-XavierHM #fault tolerance #source code #using
Using Formal Verification to Reduce Test Space of Fault-Tolerant Programs (KSX, SH, ACVdM), pp. 181–190.
HaskellHaskell-2008-MitchellR #automation #pattern matching
Not all patterns, but enough: an automatic verifier for partial but sufficient pattern matching (NM, CR), pp. 49–60.
GT-VMTGT-VMT-2006-NarayananK08 #model transformation #towards
Towards Verifying Model Transformations (AN, GK), pp. 191–200.
GT-VMTGT-VMT-2008-BaresiGMM #abstraction #graph transformation #using
Using Graph Transformation Systems to Specify and Verify Data Abstractions (LB, CG, AM, MM).
GT-VMTGT-VMT-2008-BucchiaroneG #architecture #using
Dynamic Software Architectures Verification using DynAlloy (AB, JPG).
GT-VMTGT-VMT-2008-KumarM #automaton #sequence chart
Improving Live Sequence Chart to Automata Transformation for Verification (RK, EGM).
GT-VMTGT-VMT-2008-NarayananK #model transformation
Verifying Model Transformations by Structural Correspondence (AN, GK).
ICGTICGT-2008-Aalst #consistency #workflow
Discovery, Verification and Conformance of Workflows with Cancellation (WMPvdA), pp. 18–37.
ICGTICGT-2008-Bisztray #architecture #refactoring #tool support
Verification of Architectural Refactorings: Rule Extraction and Tool Support (DB), pp. 475–477.
ICGTICGT-2008-Horvath #approach #graph transformation #towards
Towards a Two Layered Verification Approach for Compiled Graph Transformation (ÁH), pp. 499–501.
ICGTICGT-2008-KonigK #graph transformation #towards
Towards the Verification of Attributed Graph Transformation Systems (BK, VK), pp. 305–320.
ICEISICEIS-DISI-2008-SalemGB #concept #modelling #multi #specification
Multi-Dimensional Modeling — Formal Specification and Verification of the Hierarchy Concept (AS, FG, HBA), pp. 317–322.
ICEISICEIS-ISAS1-2008-MoralesTPA #communication #composition #concept #model checking
A Conceptual Scheme for Compositional Model-Checking Verification of Critical Communicating Systems (LEMM, MICT, MAP, KBA), pp. 86–93.
ICEISICEIS-ISAS2-2008-BainaT #algorithm #graph #hybrid #towards #workflow
Toward a Hybrid Algorithm for Workflow Graph Structural Verification (FT, KB, WG), pp. 442–447.
ICEISICEIS-ISAS2-2008-TobarraCPC #protocol
Formal Verification of the Secure Sockets Layer Protocol (MLT, DC, JJP, FC), pp. 246–252.
ICEISICEIS-J-2008-MoralesCPA #composition #model checking
Compositional Model-Checking Verification of Critical Systems (LEMM, MIC, MAP, KBA), pp. 213–225.
ICPRICPR-2008-IbrahimG #online #using
On-line signature verification by using most discriminating points (MTI, LG), pp. 1–4.
ICPRICPR-2008-LiuW #online
Template selection for on-line signature verification (NL, YW), pp. 1–4.
ICPRICPR-2008-MottlLSY #kernel #online
Signature verification based on fusion of on-line and off-line kernels (VM, ML, VS, AY), pp. 1–4.
ICPRICPR-2008-NeebaJ #recognition
Recognition of books by verification and retraining (NVN, CVJ), pp. 1–4.
SEKESEKE-2008-ChenLMW #algorithm #case study #optimisation #polynomial #problem
Verification of Optimization Algorithms: a Case Study of a Quadratic Assignment Problem Solver (TYC, HL, RGM, DW), pp. 16–21.
SEKESEKE-2008-GarciaRS #automation #ltl #named
PROTEF: Automatic Verification of Pattern-Based LTL Templates (LG, SR, SS), pp. 261–266.
SEKESEKE-2008-KloukinasSM #distributed #runtime
Estimating Event Lifetimes for Distributed Runtime Verification (CK, GS, KM), pp. 117–122.
SEKESEKE-2008-NakaoaTM #case study #independence #validation
Estimating the Effort of Independent Verification and Validation in the Context of Mission-critical Software Systems — A Case Study (HN, AT, JM), pp. 167–172.
SEKESEKE-2008-PengDZ #behaviour #correctness #design pattern #implementation
Verifying Behavioral Correctness of Design Pattern Implementation (TP, JD, YZ), pp. 454–459.
SEKESEKE-2008-Shaffer #domain model #security #source code #static analysis
A Security Domain Model for Static Analysis and Verification of Software Programs (ABS), pp. 673–678.
MODELSMoDELS-2008-ZamaniKB #enterprise #pattern matching
A Pattern Language Verifier for Web-Based Enterprise Applications (BZ, SK, GB), pp. 553–567.
MODELSMoDELS-2008-ZamaniKB #enterprise #pattern matching
A Pattern Language Verifier for Web-Based Enterprise Applications (BZ, SK, GB), pp. 553–567.
ECOOPECOOP-2008-DrossopoulouFMS #framework #invariant
A Unified Framework for Verification Techniques for Object Invariants (SD, AF, PM, AJS), pp. 412–437.
OOPSLAOOPSLA-2008-BeckmanBA #type system
Verifying correct usage of atomic blocks and typestate (NEB, KB, JA), pp. 227–244.
OOPSLAOOPSLA-2008-DistefanoP #java #named #towards
jStar: towards practical verification for java (DD, MJP), pp. 213–226.
AdaEuropeAdaEurope-2008-OberH #on the
On the Timed Automata-Based Verification of Ravenscar Systems (IO, NH), pp. 30–43.
PEPMPEPM-2008-PietrzakCPH #analysis #composition #prolog #source code
A practical type analysis for verification of modular prolog programs (PP, JC, GP, MVH), pp. 61–70.
PEPMPEPM-2008-SultanaT #refactoring
Mechanical verification of refactorings (NS, SJT), pp. 51–60.
PLDIPLDI-2008-ZeeKR #data type #functional #linked data #open data
Full functional verification of linked data structures (KZ, VK, MCR), pp. 349–361.
POPLPOPL-2008-ChinDNQ #composition #logic #object-oriented
Enhancing modular OO verification with separation logic (WNC, CD, HHN, SQ), pp. 87–99.
POPLPOPL-2008-LahiriQ #precise #smt #using
Back to the future: revisiting precise program verification using SMT solvers (SKL, SQ), pp. 171–182.
POPLPOPL-2008-TristanL #case study #optimisation #scheduling #validation
Formal verification of translation validators: a case study on instruction scheduling optimizations (JBT, XL), pp. 17–27.
PPDPPPDP-2008-Leuschel #declarative #programming
Declarative programming for verification: lessons and outlook (ML), pp. 1–7.
REFSQREFSQ-2008-MarincicMW #embedded #requirements
Classifying Assumptions Made during Requirements Verification of Embedded Systems (JM, AM, RW), pp. 141–146.
ASEASE-2008-BordiniDFF #automation #multi #source code
Automated Verification of Multi-Agent Programs (RHB, LAD, BF, MF), pp. 69–78.
ASEASE-2008-BordinPP #agile #modelling #prototype #realtime
Rapid Model-Driven Prototyping and Verification of High-Integrity Real-Time Systems (MB, MP, SP), pp. 491–492.
ASEASE-2008-HolzmannJG
Swarm Verification (GJH, RJ, AG), pp. 1–6.
ASEASE-2008-IspirC #aspect-oriented #programming
An Assume Guarantee Verification Methodology for Aspect-Oriented Programming (MI, ABC), pp. 391–394.
ASEASE-2008-PostS
Configuration Lifting: Verification meets Software Configuration (HP, CS), pp. 347–350.
FSEFSE-2008-YuWGB #composition #encoding #performance #summary #using #web #web service
Modular verification of web services using efficient symbolic encoding and summarization (FY, CW, AG, TB), pp. 192–202.
ICSEICSE-2008-BeekGKM
Formal verification of an automotive scenario in service-oriented computing (MHtB, SG, NK, FM), pp. 613–622.
ICSEICSE-2008-ChenDS #calculus
A verification system for timed interval calculus (CC, JSD, JS), pp. 271–280.
ICSEICSE-2008-ChenY #constraints #dependence #grid #workflow
Temporal dependency based checkpoint selection for dynamic verification of fixed-time constraints in grid workflow systems (JC, YY), pp. 141–150.
SACSAC-2008-HojjatMS #algebra #evaluation #framework #functional #performance #probability #process
A framework for performance evaluation and functional verification in stochastic process algebras (HH, MRM, MS), pp. 339–346.
SACSAC-2008-LiQWLW #consistency #diagrams #interactive #java #runtime #source code #state machine #uml
UML state machine diagram driven runtime verification of Java programs for message interaction consistency (XL, XQ, LW, BL, WEW), pp. 384–389.
SACSAC-2008-MeloNX #java #source code #testing #towards
Towards verification and testing of Java programs (ACVdM, PRFN, KSX), pp. 730–734.
SACSAC-2008-ShiYLZ #composition #semantics #web #web service
Path-based verification for composition of semantic web services (YS, JY, ZJL, JZ), pp. 2392–2396.
SACSAC-2008-XuWQ #modelling #using
Modeling and verifying BPEL using synchronized net (CX, HW, WQ), pp. 2358–2362.
GPCEGPCE-2008-DenneyF #automation #generative
Generating customized verifiers for automatically generated code (ED, BF), pp. 77–88.
CASECASE-2008-BenedettoDSW #automation #mining
Automatic verification of wireless control in a mining ventilation system (MDDB, AD, ES, EW), pp. 858–863.
CASECASE-2008-LjungkrantzAF #component #industrial #logic #programming #specification
Formal specification and verification of components for industrial logic control programming (OL, , MF), pp. 935–940.
CASECASE-2008-ZhangMT #rule-based
Verification of ECA rule based management and control systems (JZ, JRM, DMT), pp. 1–7.
CCCC-2008-MalePPD #bytecode #java
Java Bytecode Verification for @NonNull Types (CM, DJP, AP, CD), pp. 229–244.
DACDAC-2008-Beers #experience
Pre-RTL formal verification: an intel experience (RB), pp. 806–811.
DACDAC-2008-Cummings #design
SystemVerilog implicit port enhancements accelerate system design & verification (CEC), pp. 231–236.
DACDAC-2008-HaldarSPDG #c++ #modelling
Construction of concrete verification models from C++ (MH, GS, SP, BD, AG), pp. 942–947.
DACDAC-2008-HoTDDGS #identification #logic
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
Verifying really complex systems: on earth and beyond (AK, AB, DEC, RAR, RMM, AN), pp. 552–553.
DACDAC-2008-LiZY #analysis
Full-chip leakage analysis in nano-scale technologies: mechanisms, variation sources, and verification (TL, WZ, ZY), pp. 594–599.
DACDAC-2008-MenezesKA #grid #power management
A “true” electrical cell model for timing, noise, and power grid verification (NM, CVK, CSA), pp. 462–467.
DACDAC-2008-Mitra
Strategies for mainstream usage of formal verification (RSM), pp. 800–805.
DACDAC-2008-Moon #composition #optimisation
Compositional verification of retiming and sequential optimizations (IHM), pp. 131–136.
DACDAC-2008-Ng #challenge #modelling #using
Challenges in using system-level models for RTL verification (KN), pp. 812–815.
DACDAC-2008-SenOA #multi #predict #runtime
Predictive runtime verification of multi-processor SoCs in SystemC (AS, VO, MSA), pp. 948–953.
DACDAC-2008-TurumellaS #concurrent #thread
Assertion-based verification of a 32 thread SPARCTM CMT microprocessor (BT, MS), pp. 256–261.
DATEDATE-2008-ChengH #invariant #mining
Simulation-Directed Invariant Mining for Software Verification (XC, MSH), pp. 682–687.
DATEDATE-2008-FreuerJGN #constraints #design #higher-order #on the
On the Verification of High-Order Constraint Compliance in IC Design (JBF, GJ, JG, WN), pp. 26–31.
DATEDATE-2008-LaiHK #identification #multi
Improving Constant-Coefficient Multiplier Verification by Partial Product Identification (CYL, CYH, KYK), pp. 813–818.
DATEDATE-2008-LettninNRKRKSR #embedded
Verification of Temporal Properties in Automotive Embedded Software (DL, PKN, JR, TK, WR, TK, VS, SR), pp. 164–169.
DATEDATE-2008-WagnerB #adaptation #design #manycore #named
MCjammer: Adaptive Verification for Multi-core Designs (IW, VB), pp. 670–675.
DATEDATE-2008-WeinbergerBB #design #modelling #petri net #process #workflow
Application of Workflow Petri Nets to Modeling of Formal Verification Processes in Design Flow of Digital Integrated Circuits (KW, SB, RB), pp. 937–938.
PDPPDP-2008-CeccatoNT #performance #trust
Distributing Trust Verification to Increase Application Performance (MC, JN, PT), pp. 604–610.
ESOPESOP-2008-LeinoM
Verification of Equivalent-Results Methods (KRML, PM), pp. 307–321.
ESOPESOP-2008-Ong #approach #higher-order #semantics
Verification of Higher-Order Computation: A Game-Semantic Approach (CHLO), pp. 299–306.
FASEFASE-2008-BisztrayHE #architecture #refactoring
Verification of Architectural Refactorings by Rule Extraction (DB, RH, HE), pp. 347–361.
FASEFASE-2008-CiobanuK #interactive #migration #modelling
Modelling and Verification of Timed Interaction and Migration (GC, MK), pp. 215–229.
FASEFASE-2008-FantechiGLMPT #approach #model checking #specification
A Model Checking Approach for Verifying COWS Specifications (AF, SG, AL, FM, RP, FT), pp. 230–245.
FASEFASE-2008-SmansJPS #automation #java #source code
An Automatic Verifier for Java-Like Programs Based on Dynamic Frames (JS, BJ, FP, WS), pp. 261–275.
TACASTACAS-2008-AlkassarSS #pervasive
Formal Pervasive Verification of a Paging Mechanism (EA, NS, AS), pp. 109–123.
TACASTACAS-2008-FarzanCCTW #automation #composition #regular expression
Extending Automated Compositional Verification to the Full Class of ω-Regular Languages (AF, YFC, EMC, YKT, BYW), pp. 2–17.
TACASTACAS-2008-FismanKL #distributed #fault tolerance #on the #protocol
On Verifying Fault Tolerance of Distributed Protocols (DF, OK, YL), pp. 315–331.
TACASTACAS-2008-IhlemannJS #on the #reasoning
On Local Reasoning in Verification (CI, SJ, VSS), pp. 265–281.
TACASTACAS-2008-LegayMOW #automation #on the #probability #source code
On Automated Verification of Probabilistic Programs (AL, ASM, JO, JW), pp. 173–187.
TACASTACAS-2008-Malik #hardware
Hardware Verification: Techniques, Methodology and Solutions (SM), p. 1.
TACASTACAS-2008-SaksenaWJ #ad hoc #graph grammar #modelling #protocol
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols (MS, OW, BJ), pp. 18–32.
TACASTACAS-2008-WahlBE #named #symmetry
SVISS: Symbolic Verification of Symmetric Systems (TW, NB, EAE), pp. 459–462.
CAVCAV-2008-BaswanaMP #consistency #memory management #set
Implied Set Closure and Its Application to Memory Consistency Verification (SB, SKM, VP), pp. 94–106.
CAVCAV-2008-BurckhardtM #effectiveness #memory management #modelling
Effective Program Verification for Relaxed Memory Models (SB, MM), pp. 107–120.
CAVCAV-2008-CohenPZ #memory management #transaction
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses (AC, AP, LDZ), pp. 121–134.
CAVCAV-2008-Cremers #analysis #protocol #security
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols (CJFC), pp. 414–418.
CAVCAV-2008-EisnerNY #composition #design #functional #power management #reasoning
Functional Verification of Power Gated Designs by Compositional Reasoning (CE, AN, KY), pp. 433–445.
CAVCAV-2008-Foster #industrial
Assertion-Based Verification: Industry Myths to Realities (HF), pp. 5–10.
CAVCAV-2008-Harrison #proving #theorem proving
Theorem Proving for Verification (JH), pp. 11–18.
CAVCAV-2008-JoshiK #graph transformation #theorem
Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems (SJ, BK), pp. 214–226.
CAVCAV-2008-MeikleF #approach #proving
Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B (LIM, JDF), pp. 309–313.
CAVCAV-2008-NguyenC
Enhancing Program Verification with Lemmas (HHN, WNC), pp. 355–369.
CAVCAV-2008-VakkalankaGK #order #reduction #source code
Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings (SSV, GG, RMK), pp. 66–79.
ICLPICLP-2008-MontaliTACGLM #declarative #logic programming #specification #using
Verification from Declarative Specifications Using Logic Programming (MM, PT, MA, FC, MG, EL, PM), pp. 440–454.
ICSTICST-2008-RamirezC #adaptation #logic #modelling #uml
Verifying and Analyzing Adaptive Logic through UML State Models (AJR, BHCC), pp. 529–532.
ICSTICST-2008-UbayashiPST #aspect-oriented #contract #refactoring
Contract-Based Verification for Aspect-Oriented Refactoring (NU, JP, SS, TT), pp. 180–189.
IJCARIJCAR-2008-Comon-Lundh #automation #challenge #protocol #security
Challenges in the Automated Verification of Security Protocols (HCL), pp. 396–409.
IJCARIJCAR-2008-Gupta #automation #challenge
Software Verification: Roles and Challenges for Automatic Decision Procedures (AG), p. 1.
ISSTAISSTA-2008-LoginovYCFRN #analysis #safety
Verifying dereference safety via expanding-scope analysis (AL, EY, SC, SF, NR, MGN), pp. 213–224.
MBTMBT-2008-BruckerBW #empirical #proving
Verifying Test-Hypotheses: An Experiment in Test and Proof (ADB, LB, BW), pp. 15–27.
TAPTAP-2008-EngelGKR #object-oriented #testing
Integrating Verification and Testing of Object-Oriented Software (CE, CG, VK, PR), pp. 182–191.
TAPTAP-2008-Hennell #experience
The First Thirty Years: Experience with Software Verification (MAH), pp. 1–3.
FATESTestCom-FATES-2008-GrozLPS #analysis #composition #reachability #testing
Modular System Verification by Inference, Testing and Reachability Analysis (RG, KL, AP, MS), pp. 216–233.
FATESTestCom-FATES-2008-Havelund #c #runtime #source code
Runtime Verification of C Programs (KH), pp. 7–22.
VMCAIVMCAI-2008-Goldberg #on the #simulation
On Bridging Simulation and Formal Verification (EG), pp. 127–141.
VMCAIVMCAI-2008-Palsberg
Verification of Register Allocators (JP), p. 6.
CBSECBSE-2007-BaiWDTC #collaboration #contract #framework #validation #web #web service
A Framework for Contract-Based Collaborative Verification and Validation of Web Services (XB, YW, GD, WTT, YC), pp. 258–273.
ECSAECSA-2007-JeradBG #architecture #maude
Hierarchical Verification in Maude of L f P Software Architectures (CJ, KB, AGT), pp. 156–170.
ICDARICDAR-2007-AraujoCF #approach #online
An Approach to Improve Accuracy Rate of On-line Signature Verification Systems of Different Sizes (RA, GDCC, ECBCF), pp. 332–336.
ICDARICDAR-2007-BhardwajSSS #on the #using
On the Use of Lexeme Features for Writer Verification (AB, AS, HS, SNS), pp. 1088–1092.
ICDARICDAR-2007-BrinkSB #identification #towards #using
Towards Explainable Writer Verification and Identification Using Vantage Writers (AB, LS, MB), pp. 824–828.
ICDARICDAR-2007-BulacuSB #identification #independence
Text-Independent Writer Identification and Verification on Offline Arabic Handwriting (MB, LS, AB), pp. 769–773.
ICDARICDAR-2007-ChangS #online
Modified Dynamic Time Warping for Stroke-Based On-line Signature Verification (WC, JS), pp. 724–728.
ICDARICDAR-2007-CoetzerS
A Human-Centric Off-Line Signature Verification System (HC, RS), pp. 153–157.
ICDARICDAR-2007-HummIH #modelling #statistics #using
Spoken Handwriting Verification Using Statistical Models (AH, RI, JH), pp. 999–1003.
ICDARICDAR-2007-Martinez-DiazFFO #on the
On The Effects of Sampling Rate and Interpolation in HMM-Based Dynamic Signature Verification (MMD, JFA, MRF, JOG), pp. 1113–1117.
ICDARICDAR-2007-NejadR #identification
A New Method for Writer Identification and Verification Based on Farsi/Arabic Handwritten Texts (FN, MR), pp. 829–833.
ICDARICDAR-2007-NguyenBML #classification #using
Off-line Signature Verification Using Enhanced Modified Direction Features in Conjunction with Neural Classifiers and Support Vector Machines (VN, MB, VM, GL), pp. 734–738.
ICDARICDAR-2007-PapavassiliouSKC #parametricity
A Parametric Spectral-Based Method for Verification of Text in Videos (VP, TS, VK, GC), pp. 879–883.
ICDARICDAR-2007-Schomaker07a #identification #roadmap
Advances in Writer Identification and Verification (LS), pp. 1268–1273.
ICDARICDAR-2007-SrinivasanKHS #on the
On Computing Strength of Evidence for Writer Verification (HS, SK, CH, SNS), pp. 844–848.
ICDARICDAR-2007-VargasFTA07a #image #performance
Off-line Signature Verification System Performance against Image Acquisition Resolution (JFVB, MAFB, CMTG, JBA), pp. 834–838.
CSMRCSMR-2007-SzegediGBGT #concept #java #slicing #source code
Verifying the Concept of Union Slices on Java Programs (AS, TG, ÁB, TG, GT), pp. 233–242.
LATALATA-2007-TorreNPP #state machine
Verification of Succinct Hierarchical State Machines (SLT, MN, MP, GP), pp. 485–496.
IFMIFM-2007-AguirreRM #community #design
Verifying Temporal Properties of CommUnity Designs (NA, GR, TSEM), pp. 1–20.
IFMIFM-2007-BraghinSB #automation #mobile #policy #security
Automated Verification of Security Policies in Mobile Code (CB, NS, KBA), pp. 37–53.
IFMIFM-2007-Bruckner #concurrent #realtime #slicing #specification
Slicing Concurrent Real-Time System Specifications for Verification (IB), pp. 54–74.
IFMIFM-2007-FaberJS #data type #parametricity #specification
Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters (JF, SJ, VSS), pp. 233–252.
IFMIFM-2007-FehnkerHM #modelling #network #protocol
Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks (AF, LvH, AM), pp. 253–272.
IFMIFM-2007-HanebergGRS #approach #smarttech
Verifying Smart Card Applications: An ASM Approach (DH, HG, WR, GS), pp. 313–332.
IFMIFM-2007-HasanT #cumulative #probability #using
Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function (OH, ST), pp. 333–352.
IFMIFM-2007-Metzler #specification
Decomposing Integrated Specifications for Verification (BM), pp. 459–479.
IFMIFM-2007-OostdijkRTVW #encryption #learning #protocol #testing
Integrating Verification, Testing, and Learning for Cryptographic Protocols (MO, VR, JT, RGdV, TACW), pp. 538–557.
IFMIFM-2007-PodorozhnyKPZ #alloy #multi #using
Verification of Multi-agent Negotiations Using the Alloy Analyzer (RMP, SK, DEP, XZ), pp. 501–517.
IFMIFM-2007-PostK #linux #static analysis
Integrated Static Analysis for Linux Device Driver Verification (HP, WK), pp. 518–537.
RTARTA-2007-Leroy #compilation #optimisation
Formal Verification of an Optimizing Compiler (XL), p. 1.
SEFMSEFM-2007-BeckertK #concurrent #deduction #logic #source code
A Dynamic Logic for Deductive Verification of Concurrent Programs (BB, VK), pp. 141–150.
SEFMSEFM-2007-CansellGM
Formal verification of tamper-evident storage for e-voting (DC, JPG, DM), pp. 329–338.
SEFMSEFM-2007-ColvinG #algorithm #scalability #stack
A Scalable Lock-Free Stack Algorithm and its Verification (RC, LG), pp. 339–348.
SEFMSEFM-2007-CrockerC #automation #c #reasoning #source code #using
Verification of C Programs Using Automated Reasoning (DC, JC), pp. 7–14.
SEFMSEFM-2007-MehraRSJ #relational
Verification of Object Relational Maps (KKM, SKR, APS, SKJ), pp. 283–292.
SEFMSEFM-2007-SahaRC #modelling #protocol #using
Modeling and Verification of TTCAN Startup Protocol Using Synchronous Calendar (IS, SR, KC), pp. 69–79.
SEFMSEFM-2007-SalehD #approach #novel #security
Verifying Security Properties of Cryptoprotocols: A Novel Approach (MS, MD), pp. 349–360.
SEFMSEFM-2007-SchmittT #case study
Verifying the Mondex Case Study (PHS, IT), pp. 47–58.
AGTIVEAGTIVE-2007-BauerDTW #analysis #constraints #ocl #synthesis
Verification and Synthesis of OCL Constraints Via Topology Analysis (JB, WD, TT, BW), pp. 361–376.
GT-VMTGT-VMT-2007-BisztrayH #csp #process #using
Rule-Level Verification of Business Process Transformations using CSP (DB, RH).
GT-VMTGT-VMT-2007-RangelKE #approach #bisimulation
Bisimulation Verification for the DPO Approach with Borrowed (GR, BK, HE).
HCIHCI-AS-2007-LinKTKT #design #development #process #visual notation
Verification of Development of Scenarios Method and Visual Formats for Design Process (HL, MK, HT, HK, TT), pp. 1095–1101.
HCIHIMI-MTT-2007-SatoKF #concept #interface #precise
Basic Experimental Verification of Grasping Information Interface Concept, Grasping Force Increases in Precise Periods (SS, MK, YF), pp. 180–188.
CAiSECAiSE-2007-MendlingA #formal method
Formalization and Verification of EPCs with OR-Joins Based on State and Context (JM, WMPvdA), pp. 439–453.
ICEISICEIS-AIDSS-2007-Aalst #analysis #mining #process #roadmap
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-DISI-2007-Aalst #analysis #mining #process #roadmap
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-EIS-2007-Aalst #analysis #mining #process #roadmap
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-EIS-2007-CombemaleGCTV #case study #process #towards
Towards a Formal Verification of Process Model’s Properties SIMPLEPDL and TOCL Case Study (BC, PLG, XC, XT, FV), pp. 80–89.
ICEISICEIS-EIS-2007-SomeN #case study #consistency #requirements
Use Case Based Requirements Verification — Verifying the Consistency between Use Cases and Assertions (SSS, DKN), pp. 190–195.
ICEISICEIS-HCI-2007-Aalst #analysis #mining #process #roadmap
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-J-2007-CombemaleCGTV #approach #modelling #process
A Property-Driven Approach to Formal Verification of Process Models (BC, XC, PLG, XT, FV), pp. 286–300.
ICEISICEIS-SAIC-2007-Aalst #analysis #mining #process #roadmap
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-SAIC-2007-BoukadiGMB #petri net #specification #using #web #web service
Specification and Verification of Views over Composite Web Services Using High Level Petri-Nets (KB, CG, ZM, DB), pp. 107–112.
CIKMCIKM-2007-RoussinovT #online #semantics
Semantic verification in an online fact seeking environment (DR, OT), pp. 71–78.
OOPSLAOOPSLA-2007-ChenR #framework #named #performance #runtime
Mop: an efficient and generic runtime verification framework (FC, GR), pp. 569–588.
OOPSLAOOPSLA-2007-ShanerLN #composition #higher-order #source code
Modular verification of higher-order methods with mandatory calls specified by model programs (SMS, GTL, DAN), pp. 351–368.
PADLPADL-2007-AlbertGHP #analysis #bytecode #java #logic programming #source code #using
Verification of Java Bytecode Using Analysis and Transformation of Logic Programs (EA, MGZ, LH, GP), pp. 124–139.
POPLPOPL-2007-GulwaniJ #probability
Program verification as probabilistic inference (SG, NJ), pp. 277–289.
POPLPOPL-2007-ParkinsonBO #composition #stack
Modular verification of a non-blocking stack (MJP, RB, PWO), pp. 297–302.
PPDPPPDP-2007-BentonZ #compilation #formal method #semantics
Formalizing and verifying semantic type soundness of a simple compiler (NB, UZ), pp. 1–12.
SASSAS-2007-GallJ #automaton #infinity #representation
Lattice Automata: A Representation for Languages on Infinite Alphabets, and Some Applications to Verification (TLG, BJ), pp. 52–68.
SASSAS-2007-MalkisPR #precise #thread
Precise Thread-Modular Verification (AM, AP, AR), pp. 218–232.
SASSAS-2007-NandivadaPP #evaluation #framework
A Framework for End-to-End Verification and Evaluation of Register Allocators (VKN, FMQP, JP), pp. 153–169.
SASSAS-2007-ShohamG #abstraction #composition
Compositional Verification and 3-Valued Abstractions Join Forces (SS, OG), pp. 69–86.
ASEASE-2007-BarlasB #distributed #framework #java #named
Netstub: a framework for verification of distributed java applications (EB, TB), pp. 24–33.
ASEASE-2007-BlancGK #abstraction #c++
Verifying C++ with STL containers via predicate abstraction (NB, AG, DK), pp. 521–524.
ASEASE-2007-CabotCR #constraints #modelling #named #ocl #programming #uml #using
UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming (JC, RC, DR), pp. 547–548.
ASEASE-2007-Leino #specification
Specifying and verifying software (KRML), p. 2.
ESEC-FSEESEC-FSE-2007-AldrichBGLS #component #specification
Specification and verification of component-based systems 2007 (JA, MB, DG, GTL, NS), pp. 609–610.
ESEC-FSEESEC-FSE-2007-Hanna #implementation #lightweight #named #network #protocol #security
SLEDE: lightweight verification of sensor network security protocol implementations (YH), pp. 591–594.
ESEC-FSEESEC-FSE-2007-Kwiatkowska #modelling #tool support
Quantitative verification: models techniques and tools (MZK), pp. 449–458.
ESEC-FSEESEC-FSE-2007-PradellaMP #symmetry
The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties (MP, AM, PSP), pp. 312–320.
ICSEICSE-2007-BaresiGM #architecture #automation #on the
On Accurate Automatic Verification of Publish-Subscribe Architectures (LB, CG, LM), pp. 199–208.
ICSEICSE-2007-Chalin #compilation #evolution #semantics
A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler (PC), pp. 23–33.
ICSEICSE-2007-GroceHJ #difference #random #testing
Randomized Differential Testing as a Prelude to Formal Verification (AG, GJH, RJ), pp. 621–631.
SACSAC-2007-GooneratneTH #algorithm #graph #traversal #using #web #web service
Verification of web service descriptions using graph-based traversal algorithms (NG, ZT, JH), pp. 1385–1392.
SACSAC-2007-Lamari #automation #generative #model transformation #testing #towards
Towards an automated test generation for the verification of model transformations (ML), pp. 998–1005.
SACSAC-2007-Li #abstraction #parametricity #protocol #proving
Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols (YL), pp. 1534–1535.
SACSAC-2007-MorimotoSGC #security #specification
Formal verification of security specifications with common criteria (SM, SS, YG, JC), pp. 1506–1512.
SACSAC-2007-OliveiraAS #component #formal method #model checking #modelling #petri net #using
Formal modelling and verification of a component model using coloured petri nets and model checking (EASO, HOdA, LDdS), pp. 1427–1431.
SACSAC-2007-PaliwalAB #distributed #using #web #web service
Web service orchestration and verification using MSC and CP nets (AVP, NRA, CB), pp. 1693–1694.
SACSAC-2007-PloegerS #analysis #automation #documentation
Analysis and verification of an automatic document feeder (BP, LJS), pp. 1499–1505.
SACSAC-2007-RaedtsPSWSB #automation #framework
A software framework for automated verification (IR, MP, AS, JMEMvdW, LJS, MB), pp. 1031–1032.
SACSAC-2007-SantosBOJ #approach #documentation #forensics
Off-line signature verification based on forensic questioned document examination approach (CRS, FB, LSO, EJRJ), pp. 637–638.
CASECASE-2007-AnLM #collaboration #design
Expression and Verification of Task Management in Collaborative Design (YSA, RHL, AM), pp. 800–805.
CASECASE-2007-ReveliotisR0 #algebra #concurrent #correctness #policy #programming
Correctness Verification of Generalized Algebraic Deadlock Avoidance Policies through Mathematical Programming (SR, ER, JYC), pp. 200–206.
CASECASE-2007-YangM #approach #automation #feature model #interactive #matrix
Automatic Feasibility Verification of Object Configurations: A New Approach Based on Feature Interaction Matrices (FY, MMM), pp. 686–691.
COCVCOCV-2007-GallardoJM #analysis #data flow #on the fly
On-the-Fly Data Flow Analysis Based on Verification Technology (MdMG, CJ, PM), pp. 33–48.
COCVCOCV-2007-Hamilton #source code
Distilling Programs for Verification (GWH), pp. 17–32.
DACDAC-2007-BacchiniHFRLTPZ #question
Verification Coverage: When is Enough, Enough? (FB, AJH, TF, RR, DL, MT, AP, AZ), pp. 744–745.
DACDAC-2007-KasuyaT #design
Verification Methodologies in a TLM-to-RTL Design Flow (AK, TT), pp. 199–204.
DACDAC-2007-LongS
Synthesizing SVA Local Variables for Formal Verification (JL, AS), pp. 75–80.
DACDAC-2007-MathurK #design #modelling
Design for Verification in System-level Models and RTL (AM, VK), pp. 193–198.
DACDAC-2007-PetlinS #functional #multi
Functional Verification of SiCortex Multiprocessor System-on-a-Chip (OP, WS), pp. 906–909.
DACDAC-2007-Vardi
Formal Techniques for SystemC Verification; Position Paper (MYV), pp. 188–192.
DACDAC-2007-YangHH #automation #behaviour #design
Automatic Verification of External Interrupt Behaviors for Microprocessor Design (FCY, WKH, IJH), pp. 896–901.
DATEDATE-2007-Al-SammaneZT #design
A symbolic methodology for the verification of analog and mixed signal designs (GAS, MHZ, ST), pp. 249–254.
DATEDATE-2007-BronckersSPVR #analysis #interactive #simulation
Interactive presentation: Simulation methodology and experimental verification for the analysis of substrate noise on LC-VCO’s (SB, CS, GVdP, GV, YR), pp. 1520–1525.
DATEDATE-2007-LeGB #pervasive
Formal verification of a pervasive interconnect bus system in a high-performance microprocessor (TL, TG, JB), pp. 219–224.
DATEDATE-2007-LisselGG #design #industrial #perspective
Introducing new verification methods into a company’s design flow: an industrial user’s point of view (RL, JG), pp. 689–694.
WRLAWRLA-J-2004-MeseguerT07 #analysis #encryption #protocol #reachability #using
Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols (JM, PT), pp. 123–160.
WRLAWRLA-2006-SasseM07 #algebra #hoare #java #logic #semantics
Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics (RS, JM), pp. 29–46.
ESOPESOP-2007-BarthePR #bytecode #java #lightweight
A Certified Lightweight Non-interference Java Bytecode Verifier (GB, DP, TR), pp. 125–140.
ESOPESOP-2007-LeinoS #invariant #using
Using History Invariants to Verify Observers (KRML, WS), pp. 80–94.
STOCSTOC-2007-GoldwasserGHKR #constant
Verifying and decoding in constant depth (SG, DG, AH, TK, GNR), pp. 440–449.
TACASTACAS-2007-AbdullaDHR #model checking #performance #transducer
Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems) (PAA, GD, NBH, AR), pp. 721–736.
TACASTACAS-2007-CimattiRT #optimisation
Syntactic Optimizations for PSL Verification (AC, MR, ST), pp. 505–518.
TACASTACAS-2007-FriasPM #alloy #analysis #specification
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications (MFF, CLP, MMM), pp. 587–601.
TACASTACAS-2007-GheorghiuGP #composition #interface
Refining Interface Alphabets for Compositional Verification (MG, DG, CSP), pp. 292–307.
TACASTACAS-2007-GoldmanK #composition #named
MAVEN: Modular Aspect Verification (MG, SK), pp. 308–322.
TACASTACAS-2007-Leino #challenge #object-oriented
Verifying Object-Oriented Software: Lessons and Challenges (KRML), p. 2.
CADECADE-2007-GeBT #modulo theories #quantifier #satisfiability #using
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories (YG, CB, CT), pp. 167–182.
CADECADE-2007-Leino #design
Designing Verification Conditions for Software (KRML), p. 345.
CADECADE-2007-MurkLH #c #named #source code
KeY-C: A Tool for Verification of C Programs (OM, DL, RH), pp. 385–390.
CADECADE-2007-VerchinineLP #automation #deduction #proving
System for Automated Deduction (SAD): A Tool for Proof Verification (KV, AVL, AP), pp. 398–403.
CAVCAV-2007-AbdullaDR #infinity #process
Parameterized Verification of Infinite-State Processes with Global Conditions (PAA, GD, AR), pp. 145–157.
CAVCAV-2007-AmitRRSY #abstraction #comparison
Comparison Under Abstraction for Verifying Linearizability (DA, NR, TWR, MS, EY), pp. 477–490.
CAVCAV-2007-BabicH #abstraction
Structural Abstraction of Software Verification Conditions (DB, AJH), pp. 366–378.
CAVCAV-2007-BeyerHT #configuration management #convergence #model checking #program analysis
Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis (DB, TAH, GT), pp. 504–518.
CAVCAV-2007-BruttomessoCFGHNPS #industrial #lazy evaluation #problem #smt
A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems (RB, AC, AF, AG, ZH, AN, AP, RS), pp. 547–560.
CAVCAV-2007-ChakiSV #bound
Verification Across Intellectual Property Boundaries (SC, CS, HV), pp. 82–94.
CAVCAV-2007-FilliatreM #deduction #framework #platform #why
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification (JCF, CM), pp. 173–177.
CAVCAV-2007-Franzle #hybrid
Verification of Hybrid Systems (MF), p. 38.
CAVCAV-2007-GuptaMF #automation #composition #generative
Automated Assumption Generation for Compositional Verification (AG, KLM, ZF), pp. 420–432.
CAVCAV-2007-LeavensKP #behaviour #composition #functional #java #ml #specification #tutorial
A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java (GTL, JRK, EP), p. 37.
CAVCAV-2007-OuimetL #realtime #simulation #specification #tool support
The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems (MO, KL), pp. 126–130.
CAVCAV-2007-PatinST #named #parallel #recursion #source code #thread
Spade: Verification of Multithreaded Dynamic and Recursive Programs (GP, MS, TT), pp. 254–257.
CAVCAV-2007-PlakuKV #hybrid
Hybrid Systems: From Verification to Falsification (EP, LEK, MYV), pp. 463–476.
CAVCAV-2007-Russinoff #approach
A Mathematical Approach to RTL Verification (DMR), p. 2.
CAVCAV-2007-SinhaC #composition #lazy evaluation #learning #satisfiability #using
SAT-Based Compositional Verification Using Lazy Learning (NS, EMC), pp. 39–54.
ICLPICLP-2007-MancarellaTT #abduction #logic programming #web
Web Sites Verification: An Abductive Logic Programming Tool (PM, GT, FT), pp. 434–435.
MBTMBT-2007-OuimetL #automation #consistency #satisfiability #specification #state machine #using
Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver (MO, KL), pp. 85–97.
ICSTSAT-2007-Gelder #satisfiability
Verifying Propositional Unsatisfiability: Pitfalls to Avoid (AVG), pp. 328–333.
TAPTAP-2007-BackEM #invariant #source code #testing
Testing and Verifying Invariant Based Programs in the SOCOS Environment (RJB, JE, MM), pp. 61–78.
VMCAIVMCAI-2007-BouillaguetKWZR #data type #first-order #proving #theorem proving #using
Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.
VMCAIVMCAI-2007-EmmiM #transaction
Verifying Compensating Transactions (ME, RM), pp. 29–43.
VMCAIVMCAI-2007-KlaedtkeRS #abstraction #hybrid #refinement
Language-Based Abstraction Refinement for Hybrid System Verification (FK, SR, ZS), pp. 151–166.
VMCAIVMCAI-2007-Logozzo #abstract interpretation #analysis #composition #java #named
Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes (FL), pp. 283–298.
VMCAIVMCAI-2007-Madhusudan #algorithm #learning
Learning Algorithms and Formal Verification (PM), p. 214.
VMCAIVMCAI-2007-NguyenDQC #automation #logic
Automated Verification of Shape and Size Properties Via Separation Logic (HHN, CD, SQ, WNC), pp. 251–266.
VMCAIVMCAI-2007-RakamaricBH #data type #source code
An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures (ZR, JDB, AJH), pp. 106–121.
VMCAIVMCAI-2007-Revesz #approach #constraints #database
The Constraint Database Approach to Software Verification (PZR), pp. 329–345.
CBSECBSE-2006-AttieLPC #behaviour #component #design #explosion
Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based Elevator Control System (PCA, DHL, AP, HC), pp. 33–49.
CBSECBSE-2006-XieB #component #product line
Verification of Component-Based Software Application Families (FX, JCB), pp. 50–66.
DRRDRR-2006-ChenS #2d #recognition
Combining one- and two-dimensional signal recognition approaches to off-line signature verification (SC, SNS).
PODSPODS-2006-DeutschSVZ #communication #data-driven #web #web service
Verification of communicating data-driven web services (AD, LS, VV, DZ), pp. 90–99.
SIGMODSIGMOD-2006-DeutschSVZ #data-driven #interactive #specification #web
A system for specification and verification of interactive, data-driven web applications (AD, LS, VV, DZ), pp. 772–774.
ICPCICPC-2006-RooverMGGD #approach #behaviour #documentation #lightweight
An Approach to High-Level Behavioral Program Documentation Allowing Lightweight Verification (CDR, IM, KG, KG, TD), pp. 202–211.
ICALPICALP-v1-2006-AulettaPPPV
New Constructions of Mechanisms with Verification (VA, RDP, PP, GP, CV), pp. 596–607.
ICALPICALP-v2-2006-Vergnaud
New Extensions of Pairing-Based Signatures into Universal Designated Verifier Signatures (DV), pp. 58–69.
FMFM-2006-BlazyDL #c #compilation
Formal Verification of a C Compiler Front-End (SB, ZD, XL), pp. 460–475.
FMFM-2006-BotaschanjanGHKST #distributed #towards
Towards Modularized Verification of Distributed Time-Triggered Systems (JB, AG, AH, LK, MS, DT), pp. 163–178.
FMFM-2006-LiHR #automation #exception #safety #towards
Towards Automatic Exception Safety Verification (XL, HJH, PR), pp. 396–411.
FMFM-2006-PnueliZ #model checking #runtime
PSL Model Checking and Run-Time Verification Via Testers (AP, AZ), pp. 573–586.
FMFM-2006-Preoteasa #logic #pointer #recursion #using
Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic (VP), pp. 508–523.
FMFM-2006-SchmittHBRM #guidelines #interactive
Interactive Verification of Medical Guidelines (JS, AH, MB, WR, MM), pp. 32–47.
RTARTA-2006-Bryant #infinity #using
Formal Verification of Infinite State Systems Using Boolean Methods (REB), pp. 1–3.
SEFMSEFM-2006-BeckertHS #deduction #design #object-oriented
Integrating Object-Oriented Design and Deductive Verification of Software (BB, RH, PHS), p. 260.
SEFMSEFM-2006-Kapoor #formal method #modelling #pipes and filters
Formal Modelling and Verification of an Asynchronous DLX Pipeline (HKK), pp. 118–127.
SEFMSEFM-2006-MarcheR #behaviour #java #transaction
Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears (CM, NR), pp. 137–146.
SEFMSEFM-2006-RamsokulS #framework #modelling #named #protocol #web service
ASEHA: A Framework for Modelling and Verification ofWeb Services Protocols (PR, AS), pp. 196–205.
SEFMSEFM-2006-Rushby
Harnessing Disruptive Innovation in Formal Verification (JMR), pp. 21–30.
SFMSFM-2006-BombieriFP #design #hardware #simulation
Hardware Design and Simulation for Verification (NB, FF, GP), pp. 1–29.
SFMSFM-2006-CabodiM #hardware
BDD-Based Hardware Verification (GC, MM), pp. 78–107.
SFMSFM-2006-GuptaGW #hardware #satisfiability
SAT-Based Verification Methods and Applications in Hardware Verification (AG, MKG, CW), pp. 108–143.
SFMSFM-2006-Harrison #float #proving #theorem proving #using
Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.
ICFPICFP-2006-Chlipala #composition #development #proving
Modular development of certified program verifiers with a proof assistant (AC), pp. 160–171.
CAiSECAiSE-2006-WangR #modelling #workflow
Dynamic Workflow Modeling and Verification (JW, DR), pp. 303–318.
EDOCEDOC-2006-BrennerAPMMS #component #re-engineering #testing
Reducing Verification Effort in Component-Based Software Engineering through Built-In Testing (DB, CA, BP, RM, MM, DS), pp. 175–184.
ICPRICPR-v1-2006-DjiouaOP #interactive #recognition
An interactive trajectory synthesizer to study outlier patterns in handwriting recognition and signature verification (MD, CO, RP), pp. 1124–1127.
ICPRICPR-v1-2006-LlanoVKM #representation
An Illumination Insensitive Representation for Face Verification in the Frequency Domain (EGL, HMV, JK, KM), pp. 215–218.
ICPRICPR-v1-2006-WangCWG #invariant #recognition
A Verification Method for Viewpoint Invariant Sign Language Recognition (QW, XC, CW, WG), pp. 456–459.
ICPRICPR-v1-2006-ZhouW06a #using
Face Verification Using GaborWavelets and AdaBoost (MZ, HW), pp. 404–407.
ICPRICPR-v2-2006-ChenS #graph
A New Off-line Signature Verification Method based on Graph (SC, SNS), pp. 869–872.
ICPRICPR-v2-2006-KhanKKA #dependence #online
On-Line Signature Verification by Exploiting Inter-Feature Dependencies (MKK, MAK, MAUK, IA), pp. 796–799.
ICPRICPR-v2-2006-KimLKK #image #recognition #video
Stroke Verification with Gray-level Image for Hangul Video Text Recognition (JK, SL, YK, JHK), pp. 1074–1077.
ICPRICPR-v2-2006-LiuHZ #independence #robust
Robust Local Scoring Function for Text-Independent Speaker Verification (ML, TSH, ZZ), pp. 1146–1149.
ICPRICPR-v2-2006-QuanHXLL #analysis #online
Spectrum Analysis Based onWindows with Variable Widths for Online Signature Verification (ZHQ, DSH, XLX, MRL, TML), pp. 1122–1125.
ICPRICPR-v2-2006-ShimshoniRS #classification #image #performance
Efficient Search and Verification for Function Based Classification from Real Range Images (IS, ER, OS), pp. 1118–1121.
ICPRICPR-v2-2006-WeiGO #multi
Fingerprint Verification Based on Multistage Minutiae Matching (HW, MG, ZO), pp. 1058–1061.
ICPRICPR-v4-2006-ArmandBM
Off-line Signature Verification based on the Modified Direction Feature (SA, MB, VM), pp. 509–512.
ICPRICPR-v4-2006-ChaoTWC #framework #kernel #problem #testing
A Kernel-based Discrimination Framework for Solving Hypothesis Testing Problems with Application to Speaker Verification (YHC, WHT, HMW, RCC), pp. 229–232.
ICPRICPR-v4-2006-LiuXYD #hybrid
A New Hybrid GMM/SVM for Speaker Verification (ML, YX, ZY, BD), pp. 314–317.
ICPRICPR-v4-2006-NosratighodsAE #novel #set #using
Speaker Verification Using A Novel Set of Dynamic Features (MN, EA, JE), pp. 266–269.
ICPRICPR-v4-2006-RyuKJ #adaptation
Template Adaptation based Fingerprint Verification (CR, HK, AKJ), pp. 582–585.
ICPRICPR-v4-2006-ShuD #multi
Multi-Biometrics Fusion for Identity Verification (CS, XD), pp. 493–496.
ICPRICPR-v4-2006-YangG06a #multi #using
Multi-SNR GMMs-Based Noise-Robust Speaker Verification Using 1/fa Noises (LY, WG), pp. 241–244.
SEKESEKE-2006-CookeRW
The Evolutionary Role of Variable Assignment and Its Impact on Program Verification (DEC, JNR, RGW), pp. 315–320.
SEKESEKE-2006-LeeDSG #approach #modelling
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
Verifying a Software Architecture Reconstruction Framework with a Case Study (SL, SK), pp. 102–107.
MODELSMoDELS-2006-PonsG #ocl #specification
An OCL-Based Technique for Specifying and Verifying Refinement-Oriented Transformations in MDE (CP, DG), pp. 646–660.
SPLCSPLC-2006-Scheidemann #distributed #embedded #evolution #optimisation #product line
Optimizing the Selection of Representative Configurations in Verification of Evolving Product Lines of Distributed Embedded Systems (KDS), pp. 75–84.
MODELSMoDELS-2006-PonsG #ocl #specification
An OCL-Based Technique for Specifying and Verifying Refinement-Oriented Transformations in MDE (CP, DG), pp. 646–660.
AdaEuropeAdaEurope-2006-LiWQLYZZ #java #runtime #source code #specification
Runtime Verification of Java Programs for Scenario-Based Specifications (XL, LW, XQ, BL, JY, JZ, GZ), pp. 94–105.
LOPSTRLOPSTR-2006-MantelSK #data flow #proving #security
Combining Different Proof Techniques for Verifying Information Flow Security (HM, HS, TK), pp. 94–110.
PADLPADL-2006-Wang #automation #model checking
Automatic Verification of a Model Checker by Reflection (BYW), pp. 45–59.
PLDIPLDI-2006-FengSVXN #abstraction #assembly #composition
Modular verification of assembly code with stack-based control abstractions (XF, ZS, AV, SX, ZN), pp. 401–414.
POPLPOPL-2006-LahiriQ
Verifying properties of well-founded linked lists (SKL, SQ), pp. 115–126.
PPDPPPDP-2006-AlbertiGLCMM #abduction #framework #web #web service
An abductive framework for a-priori verification of web services (MA, MG, EL, FC, PM, MM), pp. 39–50.
SASSAS-2006-LoginovRS #algorithm #automation
Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm (AL, TWR, MS), pp. 261–279.
ASEASE-2006-Futatsugi #proving #specification
Verifying Specifications with Proof Scores in CafeOBJ (KF), pp. 3–10.
ASEASE-2006-TateishiMOS #automation
Automated Verification Tool for DHTML (TT, HM, KO, SS), pp. 363–364.
ICSEICSE-2006-BeckerBGKS #adaptation #invariant
Symbolic invariant verification for systems with dynamic structural adaptation (BB, DB, HG, FK, DS), pp. 72–81.
ICSEICSE-2006-FosterUMK #composition #modelling #named #web #web service
LTSA-WS: a tool for model-based verification of web service compositions and choreography (HF, SU, JM, JK), pp. 771–774.
ICSEICSE-2006-TanAC #finite
Managing space for finite-state verification (JT, GSA, LAC), pp. 152–161.
ICSEICSE-2006-Yin #approach
The echo approach to formal verification (XY), pp. 981–984.
SACSAC-2006-BurdyP #bytecode #java #specification
Java bytecode specification and verification (LB, MP), pp. 1835–1839.
SACSAC-2006-DinechinLM #using
Assisted verification of elementary functions using Gappa (FdD, CQL, GM), pp. 1318–1322.
SACSAC-2006-FilhoRR #coordination #exception
Verification of coordinated exception handling (FCF, AR, CMFR), pp. 680–685.
SACSAC-2006-MalgouyresM #approach #consistency #formal method #metamodelling #uml
A UML model consistency verification approach based on meta-modeling formalization (HM, GM), pp. 1804–1809.
SACSAC-2006-MorimotoSGC #security #specification #standard
A security specification verification technique based on the international standard ISO/IEC 15408 (SM, SS, YG, JC), pp. 1802–1803.
SACSAC-2006-NasrBFI #automaton #specification
Verification of a scheduler in B through a timed automata specification (ON, JPB, MF, MRI), pp. 1800–1801.
GPCEGPCE-2006-CzarneckiP #constraints #ocl
Verifying feature-based model templates against well-formedness OCL constraints (KC, KP), pp. 211–220.
GPCEGPCE-2006-LeavensABBCFHJMJSSS #roadmap
Roadmap for enhanced languages and methods to aid verification (GTL, JRA, DSB, MJB, AC, KF, ECRH, CBJ, DM, SLPJ, MS, DRS, AS), pp. 221–236.
DACDAC-2006-BergeronFPMAS #testing
Building a verification test plan: trading brute force for finesse (JB, HF, AP, RSM, CA, DS), pp. 805–806.
DACDAC-2006-BrierM #architecture #c #c++ #modelling #using
Use of C/C++ models for architecture exploration and verification of DSPs (DB, RSM), pp. 79–84.
DACDAC-2006-DupenloupLM #abstraction #functional
Transistor abstraction for the functional verification of FPGAs (GD, TL, RM), pp. 1069–1072.
DACDAC-2006-FengH #equivalence
Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification (XF, AJH), pp. 1063–1068.
DACDAC-2006-Gluska
Practical methods in coverage-oriented verification of the merom microprocessor (AG), pp. 332–337.
DACDAC-2006-GoraiBBTM #protocol
Directed-simulation assisted formal verification of serial protocol and bridge (SG, SB, LB, PT, RSM), pp. 731–736.
DACDAC-2006-HosseiniPCUGB #design #question #standard
Building a standard ESL design and verification methodology: is it just a dream? (AH, AP, HTC, PU, EFG, SB), pp. 370–371.
DACDAC-2006-NahirZEKR #generative #multi #testing
Scheduling-based test-case generation for verification of multimedia SoCs (AN, AZ, RE, TK, NR), pp. 348–351.
DACDAC-2006-ShimizuGKOAMS
Verification of the cell broadband engineTM processor (KS, SG, TK, TO, JA, LM, TS), pp. 338–343.
DACDAC-2006-Swan #modelling #transaction
SystemC transaction level models and RTL verification (SS), pp. 90–92.
DATEDATE-2006-BalarinP #functional #generative #interface #specification
Functional verification methodology based on formal interface specification and transactor generation (FB, RP), pp. 1013–1018.
DATEDATE-2006-BombieriFP #evaluation #on the #reuse
On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL (NB, FF, GP), pp. 1007–1012.
DATEDATE-2006-FeyGD
Avoiding false negatives in formal verification for protocol-driven blocks (GF, DG, RD), pp. 1225–1226.
DATEDATE-2006-FrehseKR #abstraction #refinement #using
Verifying analog oscillator circuits using forward/backward abstraction refinement (GF, BHK, RAR), pp. 257–262.
DATEDATE-2006-HabibiTSLM #performance #using
Efficient assertion based verification using TLM (AH, ST, AS, DL, OAM), pp. 106–111.
DATEDATE-2006-HassenT #on the #probability #term rewriting
On the numerical verification of probabilistic rewriting systems (JBH, ST), pp. 1223–1224.
DATEDATE-2006-JerinicLHM #functional #metric
New methods and coverage metrics for functional verification (VJ, JL, UH, DM), pp. 1025–1030.
DATEDATE-2006-KaneMS #pipes and filters
Monolithic verification of deep pipelines with collapsed flushing (RK, PM, SKS), pp. 1234–1239.
DATEDATE-2006-KarlssonEP #design #petri net #representation #using
Formal verification of systemc designs using a petri-net based representation (DK, PE, ZP), pp. 1228–1233.
DATEDATE-2006-MatulaM #algorithm #float #formal method #generative #performance #standard #traversal
A formal model and efficient traversal algorithm for generating testbenches for verification of IEEE standard floating point division (DWM, LDM), pp. 1134–1138.
DATEDATE-2006-ShekharKE #equivalence #multi
Equivalence verification of arithmetic datapaths with multiple word-length operands (NS, PK, FE), pp. 824–829.
DATEDATE-2006-ShyamB #hybrid
Distance-guided hybrid verification with GUIDO (SS, VB), pp. 1211–1216.
DATEDATE-2006-WangYIG #embedded #image
Disjunctive image computation for embedded software verification (CW, ZY, FI, AG), pp. 1205–1210.
DATEDATE-DF-2006-BonfiniCMP
A mixed-signal verification kit for verification of analogue-digital circuits (GB, MC, RM, EP), pp. 88–93.
DATEDATE-DF-2006-Daglio #design #embedded
A complete and fully qualified design flow for verification of mixed-signal SoC with embedded flash memories (PD), pp. 94–99.
DATEDATE-DF-2006-HuttonYSBCCP #synthesis
A methodology for FPGA to structured-ASIC synthesis and verification (MH, RY, JS, GB, SC, KKC, HKP), pp. 64–69.
DATEDATE-DF-2006-ZarriCDMPRT #on the #protocol
On the verification of automotive protocols (GZ, FC, FD, RM, MP, GR, CT), pp. 195–200.
HPCAHPCA-2006-ManovitH #consistency #memory management
Completely verifying memory consistency of test program executions (CM, SH), pp. 166–175.
ESOPESOP-2006-LeinoM
A Verification Methodology for Model Fields (KRML,