BibSLEIGH — verification tag

verification

verification

Tag #verification

2955 papers:

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