BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Used together with:
system (376)
base (270)
use (259)
formal (252)
model (250)

Stem verif$ (all stems)

2186 papers:

CASECASE-2015-JiangDZZ #formal method #mobile #modelling #verification
Formal modeling and verification of secure mobile agent systems (MJ, ZD, MZ, YZ), pp. 545–550.
CASECASE-2015-Malik #composition #verification
Advanced selfloop removal in compositional nonblocking verification of discrete event systems (RM), pp. 819–824.
DACDAC-2015-CiesielskiYBLR #verification
Verification of gate-level arithmetic circuits by function extraction (MJC, CY, WB, DL, AR), p. 6.
DACDAC-2015-EspinosaHAAR #analysis #correlation #robust #set #verification
Analysis and RTL correlation of instruction set simulators for automotive microcontroller robustness verification (JE, CH, JA, DdA, JCR), p. 6.
DACDAC-2015-Foster #functional #industrial #roadmap #verification
Trends in functional verification: a 2014 industry study (HDF), p. 6.
DACDAC-2015-GuoDJFM #formal method #perspective #security #validation #verification
Pre-silicon security verification and validation: a formal perspective (XG, RGD, YJ, FF, PM), p. 6.
DACDAC-2015-KleebergerRC #design #verification
Design & verification of automotive SoC firmware (VBK, SR, RC), p. 6.
DACDAC-2015-TodmanSL #configuration management #design #monitoring #runtime #verification
In-circuit temporal monitors for runtime verification of reconfigurable designs (TT, SS, WL), p. 6.
DACDAC-2015-XiaoGWYTW #layout #optimisation #self #verification
Layout optimization and template pattern verification for directed self-assembly (DSA) (ZX, DG, MDFW, HY, MCT, HSPW), p. 6.
DACDAC-2015-ZhengLDGZS #design #security #verification
Design and verification for transportation system security (BZ, WL, PD, LG, QZ, NS), p. 6.
DATEDATE-2015-BergmanBKKMNOPR #experience #industrial #verification
Designer-level verification: an industrial experience story (SB, GB, WK, SK, SM, ZN, AO, VP, WR, GS, VV), pp. 410–411.
DATEDATE-2015-BombieriFPS #abstraction #verification
RTL property abstraction for TLM assertion-based verification (NB, RF, GP, FS), pp. 85–90.
DATEDATE-2015-BurnsSY #modelling #synthesis #verification
GALS synthesis and verification for xMAS models (FPB, DS, AY), pp. 1419–1424.
DATEDATE-2015-KimFPSL #framework #implementation #modelling #verification
Platform-specific timing verification framework in model-based implementation (BK, LF, LTXP, OS, IL), pp. 235–240.
DATEDATE-2015-KonstantinouKM #encryption #functional #privacy #verification
Privacy-preserving functional IP verification utilizing fully homomorphic encryption (CK, AK, MM), pp. 333–338.
DATEDATE-2015-KroeningLMST #bytecode #effectiveness #low level #verification
Effective verification of low-level software with nested interrupts (DK, LL, TM, PS, MT), pp. 229–234.
DATEDATE-2015-KumarLSSH #adaptation #verification
Timing verification for adaptive integrated circuits (RK, BL, YS, US, JH), pp. 1587–1590.
DATEDATE-2015-ShonikerCHP #design #process #simulation #verification
Minimizing the number of process corner simulations during design verification (MS, BFC, JH, WP), pp. 289–292.
DATEDATE-2015-SunKPE #algebra #geometry #using #verification
Formal verification of sequential Galois field arithmetic circuits using algebraic geometry (XS, PK, TP, FE), pp. 1623–1628.
ESOPESOP-2015-Penninckx0P #behaviour #composition #source code #verification
Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs (WP, BJ, FP), pp. 158–182.
FASEFASE-2015-BlomDH #verification
Verification of Loop Parallelisations (SB, SD, MH), pp. 202–217.
TACASTACAS-2015-AledoE #contest #embedded #framework #verification
FramewORk for Embedded System verification — (Competition Contribution) (PGdA, PSE), pp. 429–431.
TACASTACAS-2015-ArmandoBCCMMM #framework #mobile #named #security #static analysis #verification
SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform (AA, GB, GC, GC, GDM, RM, AM), pp. 225–230.
TACASTACAS-2015-Beyer #verification
Software Verification and Verifiable Witnesses — (Report on SV-COMP 2015) (DB), pp. 401–416.
TACASTACAS-2015-CiniF #ltl #proving #runtime #verification
An LTL Proof System for Runtime Verification (CC, AF), pp. 581–595.
TACASTACAS-2015-DuggiralaMVP #modelling #named #verification
C2E2: A Verification Tool for Stateflow Models (PSD, SM, MV, MP), pp. 68–82.
TACASTACAS-2015-KriouileS #formal method #using #verification
Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip (AK, WS), pp. 708–722.
TACASTACAS-2015-TschannenFNP #functional #named #object-oriented #source code #verification
AutoProof: Auto-Active Functional Verification of Object-Oriented Programs (JT, CAF, MN, NP), pp. 566–580.
ICSMEICSME-2015-MedicherlaKN #specification #using #verification
Program specialization and verification using file format specifications (RKM, RK, SN), pp. 191–200.
PEPMPEPM-2015-KafleG #constraints #horn clause #verification
Constraint Specialisation in Horn Clause Verification (BK, JPG), pp. 85–90.
PEPMPEPM-2015-LeCT #concurrent #thread #verification
Threads as Resource for Concurrency Verification (DKL, WNC, YMT), pp. 73–84.
PLDIPLDI-2015-Appel #encryption #verification
Verification of a cryptographic primitive: SHA-256 (abstract) (AWA), p. 153.
PLDIPLDI-2015-SergeyNB #concurrent #fine-grained #source code #verification
Mechanized verification of fine-grained concurrent programs (IS, AN, AB), pp. 77–87.
PLDIPLDI-2015-SharmaBA #gpu #source code #verification
Verification of producer-consumer synchronization in GPU programs (RS, MB, AA), pp. 88–98.
SASSAS-2015-Brain0KS #invariant #safety #verification
Safety Verification and Refutation by k-Invariants and k-Induction (MB, SJ, DK, PS), pp. 145–161.
SASSAS-2015-Terauchi #effectiveness #heuristic #refinement #verification
Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR (TT), pp. 128–144.
LATALATA-2015-FarzanHHKP #automation #verification
Automated Program Verification (AF, MH, JH, ZK, AP), pp. 25–46.
FMFM-2015-AhrendtCPS #runtime #specification #verification
A Specification Language for Static and Runtime Verification of Data and Control Properties (WA, JMC, GJP, GS), pp. 108–125.
FMFM-2015-AlTurkiA #distributed #framework #towards #using #verification #𝕂
Towards Formal Verification of Orchestration Computations Using the 𝕂 Framework (MAA, OA), pp. 40–56.
FMFM-2015-BagheriKMJ #android #bound #design #detection #protocol #verification
Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification (HB, EK, SM, DJ), pp. 73–89.
FMFM-2015-Damm #analysis #automation #lessons learnt #named #verification
AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned (WD), pp. 18–19.
FMFM-2015-FernandezAKK #automation #verification
Automated Verification of RPC Stub Code (MF, JA, GK, IK), pp. 273–290.
FMFM-2015-Lecomte #modelling #verification
Formal Virtual Modelling and Data Verification for Supervision Systems (TL), pp. 597–600.
FMFM-2015-SogokonJ #hybrid #liveness #verification
Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems (AS, PBJ), pp. 514–531.
SEFMSEFM-2015-AmighiDBH #source code #specification #verification
Specification and Verification of Atomic Operations in GPGPU Programs (AA, SD, SB, MH), pp. 69–83.
SEFMSEFM-2015-BlomHZ #behaviour #concurrent #functional #source code #verification
History-Based Verification of Functional Behaviour of Concurrent Programs (SB, MH, MZS), pp. 84–98.
SEFMSEFM-2015-ClarisoGC #bound #ocl #refinement #towards #uml #verification
Towards Domain Refinement for UML/OCL Bounded Verification (RC, CAG, JC), pp. 108–114.
SEFMSEFM-2015-ColomboDF #runtime #verification
Investigating Instrumentation Techniques for ESB Runtime Verification (CC, GD, AF), pp. 99–107.
GaMGaM-2015-HeussnerPCM #concurrent #graph #object-oriented #towards #verification
Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model (AH, CMP, CC, BM), pp. 32–47.
ICGTICGT-2015-KwantesGKR #modelling #process #towards #verification
Towards Compliance Verification Between Global and Local Process Models (PMK, PVG, JK, AR), pp. 221–236.
HCIDUXU-UI-2015-HwangLJ #difference #gender #smarttech #user interface #verification #women
Verification of Stereotype on Women Observing Gender Difference on UX of Wearable Device (HJH, JML, DYJ), pp. 214–223.
CAiSECAiSE-2015-DelmasP #policy #requirements #verification
Need-to-Share and Non-diffusion Requirements Verification in Exchange Policies (RD, TP), pp. 151–165.
CAiSECAiSE-2015-EstanolST #modelling #process #uml #validation #verification
Verification and Validation of UML Artifact-Centric Business Process Models (ME, MRS, ET), pp. 434–449.
ICEISICEIS-v3-2015-PassosJ #process #verification #workflow
Relaxed Soundness Verification for Interorganizational Workflow Processes (LMSP, SJ), pp. 221–228.
SEKESEKE-2015-XiangQB #flexibility #java #runtime #verification
Flexible and Extensible Runtime Verification for Java (CX, ZQ, WB), pp. 595–600.
ECMFAECMFA-J-2012-BaresiBKMMPRR15 #approach #embedded #uml #validation #verification
Formal verification and validation of embedded systems: the UML-based MADES approach (LB, GB, DSK, NDM, AM, RFP, AR, MR), pp. 343–363.
AMTAMT-2015-DyckGLSG #automation #behaviour #model transformation #towards #verification
Towards the Automatic Verification of Behavior Preservation at the Transformation Level for Operational Model Transformations (JD, HG, LL, SS, SG), pp. 36–45.
AMTAMT-2015-SelimCDLO #case study #debugging #experience #model transformation #verification
Finding and Fixing Bugs in Model Transformations with Formal Verification: An Experience Report (GMKS, JRC, JD, LL, BJO), pp. 26–35.
ECOOPECOOP-2015-BostromM #composition #finite #source code #verification
Modular Verification of Finite Blocking in Non-terminating Programs (PB, PM), pp. 639–663.
ECOOPECOOP-2015-JacobsBK #composition #termination #verification
Modular Termination Verification (BJ, DB, RK), pp. 664–688.
ECOOPECOOP-2015-Summers #stack #verification
Software Verification “Across the Stack” (Invited Talk) (AJS), p. 3.
OOPSLAOOPSLA-2015-LopezMMNSVY #message passing #parallel #source code #verification
Protocol-based verification of message-passing parallel programs (HAL, ERBM, FM, NN, CS, VTV, NY), pp. 280–298.
PPDPPPDP-2015-Al-HumaimeedyF #multi #specification #verification
Enhancing the specification and verification techniques of multiparty sessions in SOC (ASAH, MF), pp. 19–30.
PPDPPPDP-2015-AngelisFPP #generative #semantics #verification
Semantics-based generation of verification conditions by program specialization (EDA, FF, AP, MP), pp. 91–102.
PPDPPPDP-2015-ChenLJZL #automation #declarative #network #safety #source code #verification
Automated verification of safety properties of declarative networking programs (CC, LKL, LJ, WZ, BTL), pp. 79–90.
PPDPPPDP-2015-Cousot #abstract interpretation #induction #verification
Verification by abstract interpretation, soundness and abstract induction (PC), pp. 1–4.
POPLPOPL-2015-Agten0P #c #composition #verification
Sound Modular Verification of C Code Executing in an Unverified Context (PA, BJ, FP), pp. 581–594.
POPLPOPL-2015-Chlipala15a #case study #composition #interface #network #parallel #thread #verification #web
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification (AC), pp. 609–622.
SACSAC-2015-DiazCMR #architecture #model checking #verification #web #web service
Model-checking verification of publish-subscribe architectures in web service contexts (GD, MEC, HM, VVR), pp. 1688–1695.
ICSEICSE-v1-2015-BaresiKR #ltl #performance #scalability #specification #verification
Efficient Scalable Verification of LTL Specifications (LB, MMPK, MR), pp. 711–721.
ICSEICSE-v1-2015-BocicB #performance #verification
Coexecutability for Efficient Verification of Data Model Updates (IB, TB), pp. 744–754.
ICSEICSE-v1-2015-MatichukMAJKS #empirical #formal method #towards #verification
Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification (DM, TCM, JA, DRJ, GK, MS), pp. 722–732.
ICSEICSE-v2-2015-Kallehbasti #modelling #scalability #uml #verification
Scalable Formal Verification of UML Models (MMPK), pp. 847–850.
ICSEICSE-v2-2015-Merwe #android #verification
Verification of Android Applications (HvdM), pp. 931–934.
ASPLOSASPLOS-2015-FletcherRKDD #ram #recursion #verification
Freecursive ORAM: [Nearly] Free Recursion and Integrity Verification for Position-based Oblivious RAM (CWF, LR, AK, MvD, SD), pp. 103–116.
LCTESLCTES-2015-ProcterHGBA #design #hardware #implementation #semantics #verification
Semantics Driven Hardware Design, Implementation, and Verification with ReWire (AMP, WLH, IG, MB, GA), p. 10.
PPoPPPPoPP-2015-CogumbreiroHMY #concurrent #verification
Dynamic deadlock verification for general barrier synchronisation (TC, RH, FM, NY), pp. 150–160.
CADECADE-2015-DinBH #concurrent #deduction #modelling #named #verification
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS (CCD, RB, RH), pp. 517–526.
CAVCAV-2015-ChatterjeeIP #algorithm #constant #graph #performance #verification
Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs (KC, RIJ, AP), pp. 140–157.
CAVCAV-2015-CookKP #automation #infinity #on the #verification
On Automation of CTL* Verification for Infinite-State Systems (BC, HK, NP), pp. 13–29.
CAVCAV-2015-DasLLL #precise #verification
Angelic Verification: Precise Verification Modulo Unknowns (AD, SKL, AL, YL), pp. 324–342.
CAVCAV-2015-DemyanovaPVZ #benchmark #empirical #metric #tool support #verification
Empirical Software Metrics for Benchmarking of Verification Tools (YD, TP, HV, FZ), pp. 561–579.
CAVCAV-2015-DuggiralaFM0 #challenge #verification
Meeting a Powertrain Verification Challenge (PSD, CF, SM, MV), pp. 536–543.
CAVCAV-2015-GleissenthallKR #verification
Symbolic Polytopes for Quantitative Interpolation and Verification (KvG, BK, AR), pp. 178–194.
CAVCAV-2015-GurfinkelKKN #framework #verification
The SeaHorn Verification Framework (AG, TK, AK, JAN), pp. 343–361.
CAVCAV-2015-LeinoW #fine-grained #verification
Fine-Grained Caching of Verification Results (KRML, VW), pp. 380–397.
CAVCAV-2015-VijayaraghavanC #composition #deduction #design #hardware #multi #verification
Modular Deductive Verification of Multiprocessor Hardware Designs (MV, AC, A, ND), pp. 109–127.
CAVCAV-2015-ZouFZM #automation #difference #equation #safety #verification
Automatic Verification of Stability and Safety for Delay Differential Equations (LZ, MF, NZ, PNM), pp. 338–355.
ISSTAISSTA-2015-DimjasevicG #analysis #assurance #generative #runtime #testing #verification
Test-case generation for runtime analysis and vice versa: verification of aircraft separation assurance (MD, DG), pp. 282–292.
TAPTAP-2015-GenestierGP #array #deduction #generative #verification
Sequential Generation of Structured Arrays and Its Deductive Verification (RG, AG, GP), pp. 109–128.
VMCAIVMCAI-2015-CortesiFPT #mobile #policy #privacy #semantics #verification
Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications (AC, PF, MP, OT), pp. 61–79.
VMCAIVMCAI-2015-DanMVY #abstraction #effectiveness #memory management #modelling #verification
Effective Abstractions for Verification under Relaxed Memory Models (AMD, YM, MTV, EY), pp. 449–466.
VMCAIVMCAI-2015-GjomemoNPVZ #optimisation #verification
From Verification to Optimizations (RG, KSN, PHP, VNV, LDZ), pp. 300–317.
VMCAIVMCAI-2015-KafleG #horn clause #refinement #verification
Tree Automata-Based Refinement with Application to Horn Clause Verification (BK, JPG), pp. 209–226.
QoSAQoSA-2014-JohnsenLPH #dependence #graph #modelling #slicing #verification
Regression verification of AADL models through slicing of system dependence graphs (AJ, KL, PP, KH), pp. 103–112.
ASEASE-2014-BasuB #automation #bound #interactive #verification
Automatic verification of interactions in asynchronous systems with unbounded buffers (SB, TB), pp. 743–754.
ASEASE-2014-FelsingGKRU #automation #verification
Automating regression verification (DF, SG, VK, PR, MU), pp. 349–360.
ASEASE-2014-Lopez-FernandezGL #metamodelling #validation #verification
Meta-Model validation and verification with MetaBest (JJLF, EG, JdL), pp. 831–834.
ASEASE-2014-MolotnikovVR #automation #c #verification
Automated domain-specific C verification with mbeddr (ZM, MV, DR), pp. 539–550.
DACDAC-2014-AdirGHHHHKKLMNPSOTTZ #memory management #transaction #verification
Verification of Transactional Memory in POWER8 (AA, DG, DH, OH, BGH, KH, WK, AK, JML, CM, AN, RRP, MS, BSO, BWT, ET, AZ), p. 6.
DACDAC-2014-ChenWLZAMWH #functional #multi #prototype #standard #verification
A SystemC Virtual Prototyping based Methodology for Multi-Standard SoC Functional Verification (ZC, YW, LL, YZ, AA, JHM, RW, SH), p. 6.
DACDAC-2014-KoestersG #verification
Verification of Non-Mainline Functions in Todays Processor Chips (JK, AG), p. 3.
DACDAC-2014-KrautzPAKPB #automation #float #verification
Automatic Verification of Floating Point Units (UK, VP, AA, SK, SP, TB), p. 6.
DACDAC-2014-LinL #analysis #parallel #reachability #verification
Parallel Hierarchical Reachability Analysis for Analog Verification (HL, PL), p. 6.
DACDAC-2014-PrussKE #abstraction #equivalence #scalability #using #verification
Equivalence Verification of Large Galois Field Arithmetic Circuits using Word-Level Abstraction via Gröbner Bases (TP, PK, FE), p. 6.
DACDAC-2014-Rodriguez-NavasSHNLL #approach #automation #functional #safety #specification #verification
Automated Specification and Verification of Functional Safety in Heavy-Vehicles: the VeriSpec Approach (GRN, CCS, HH, MN, OL, HL), p. 4.
DACDAC-2014-XiaoDTWYWZ #self #verification
Directed Self-Assembly (DSA) Template Pattern Verification (ZX, YD, HT, MDFW, HY, HSPW, HZ), p. 6.
DATEDATE-2014-BurlyaevFG
Verification-guided voter minimization in triple-modular redundant circuits (DB, PF, AG), pp. 1–6.
DATEDATE-2014-GuarnieriPSVBFMP #embedded #monitoring #verification
A cross-level verification methodology for digital IPs augmented with embedded timing monitors (VG, MP, AS, SV, NB, FF, EM, MP), pp. 1–6.
DATEDATE-2014-JoostenS #communication #liveness #scalability #verification
Scalable liveness verification for communication fabrics (SJCJ, JS), pp. 1–6.
DATEDATE-2014-KauerSGCA #distributed #embedded #fault tolerance #synthesis #verification
Fault-tolerant control synthesis and verification of distributed embedded systems (MK, DS, DG, SC, AMA), pp. 1–6.
DATEDATE-2014-SubramanyanA #design #security #verification
Formal verification of taint-propagation security properties in a commercial SoC design (PS, DA), pp. 1–2.
DATEDATE-2014-WelpK #invariant #refinement #verification
Property directed invariant refinement for program verification (TW, AK), pp. 1–6.
DRRDRR-2014-LiPLD #analysis #online #verification
On-line signature verification method by Laplacian spectral analysis and dynamic time warping (CL, LP, CL, XD), p. ?–10.
ESOPESOP-2014-KuwaharaTU0 #automation #functional #higher-order #source code #termination #verification
Automatic Termination Verification for Higher-Order Functional Programs (TK, TT, HU, NK), pp. 392–411.
FASEFASE-2014-MasciZJCT #user interface #using #verification
Formal Verification of Medical Device User Interfaces Using PVS (PM, YZ, PLJ, PC, HWT), pp. 200–214.
TACASTACAS-2014-Ardeshir-LarijaniGN #concurrent #equivalence #protocol #quantum #verification
Verification of Concurrent Quantum Protocols by Equivalence Checking (EAL, SJG, RN), pp. 500–514.
TACASTACAS-2014-Beyer #contest #summary #verification
Status Report on Software Verification — (Competition Summary SV-COMP 2014) (DB0), pp. 373–388.
TACASTACAS-2014-EldibWS #smt #verification
SMT-Based Verification of Software Countermeasures against Side-Channel Attacks (HE, CW, PS), pp. 62–77.
TACASTACAS-2014-GurfinkelB #contest #named #verification
FrankenBit: Bit-Precise Verification with Many Bits — (Competition Contribution) (AG, AB), pp. 408–411.
TACASTACAS-2014-HartmannsH #ide #modelling #tool support #verification
The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification (AH, HH), pp. 593–598.
TACASTACAS-2014-PiskacWZ #named #specification #verification
GRASShopper — Complete Heap Verification with Mixed Specifications (RP, TW, DZ), pp. 124–139.
TACASTACAS-2014-Siirtola #bound #composition #multi #named #verification
Bounds2: A Tool for Compositional Multi-parametrised Verification (AS), pp. 599–604.
SCAMSCAM-2014-TliliFBDH #scalability #security #verification
Scalable Security Verification of Software at Compile Time (ST, JMF, AB, BD, SH), pp. 115–124.
PEPMPEPM-J-2013-AngelisFPP14 #verification
Program verification via iterated specialization (EDA, FF, AP, MP), pp. 149–175.
PLDIPLDI-2014-Carbonneaux0RS #bound #c #source code #verification
End-to-end verification of stack-space bounds for C programs (QC, JH, TR, ZS), p. 30.
PLDIPLDI-2014-GreenawayLAK #c #verification
Don’t sweat the small stuff: formal verification of C code without the pain (DG, JL, JA, GK), p. 45.
PLDIPLDI-2014-LogozzoLFB #towards #verification
Verification modulo versions: towards usable verification (FL, SKL, MF, SB), p. 32.
SASSAS-2014-AbdullaHH #exclamation #verification
Block Me If You Can! — Context-Sensitive Parameterized Verification (PAA, FH, LH), pp. 1–17.
LATALATA-2014-GantyR #order #verification
Ordered Counter-Abstraction — Refinable Subword Relations for Parameterized Verification (PG, AR), pp. 396–408.
FMFM-2014-ArenisWDMA #consistency #industrial #standard #verification
The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification (SFA, BW, DD, MM, ASA), pp. 658–672.
FMFM-2014-ArmstrongGS #algebra #concurrent #tool support #verification
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools (AA, VBFG, GS), pp. 78–93.
FMFM-2014-BlomH #concurrent #source code #verification
The VerCors Tool for Verification of Concurrent Programs (SB, MH), pp. 127–131.
FMFM-2014-LiuXZS #verification
Formal Verification of Operational Transformation (YL, YX, SJZ, CS), pp. 432–448.
FMFM-2014-MaricS #hardware #memory management #transaction #verification
Verification of a Transactional Memory Manager under Hardware Failures and Restarts (OM, CS), pp. 449–464.
FMFM-2014-ShanWFZZWQC #using #verification
Formal Verification of Lunar Rover Control Software Using UPPAAL (LS, YW, NF, XZ, LZ, LW, LQ, JC), pp. 718–732.
FMFM-2014-ZhaoYZGZC #verification
Formal Verification of a Descent Guidance Control Program of a Lunar Lander (HZ, MY, NZ, BG, LZ, YC), pp. 733–748.
IFMIFM-2014-HentschelKHB #ide #interactive #verification
An Interactive Verification Tool Meets an IDE (MH, SK, RH, RB), pp. 55–70.
IFMIFM-2014-JakobsPWW #hardware #verification
Integrating Software and Hardware Verification (MCJ, MP, HW, TW), pp. 307–322.
SEFMSEFM-2014-ArmstrongGS #higher-order #lightweight #tool support #verification
Lightweight Program Construction and Verification Tools in Isabelle/HOL (AA, VBFG, GS), pp. 5–19.
SEFMSEFM-2014-HauzarK #named #php #verification #web
WeVerca: Web Applications Verification for PHP (DH, JK), pp. 296–301.
SEFMSEFM-2014-LaibinisTGMK #behaviour #formal method #modelling #verification
Formal Modelling and Verification of Cooperative Ant Behaviour in Event-B (LL, ET, ZG, FM, AHK), pp. 363–377.
SEFMSEFM-2014-Leroy #code generation #proving #tool support #verification
Formal Proofs of Code Generation and Verification Tools (XL), pp. 1–4.
SEFMSEFM-2014-ReicherdtG #matlab #modelling #using #verification
Formal Verification of Discrete-Time MATLAB/Simulink Models Using Boogie (RR, SG), pp. 190–204.
SEFMSEFM-2014-RodriguezFHM #erlang #execution #state machine #uml #verification
Execution and Verification of UML State Machines with Erlang (RJR, LÅF, ÁHN, JM), pp. 284–289.
SEFMSEFM-2014-TatsutaC #induction #logic #verification
Completeness of Separation Logic with Inductive Definitions for Program Verification (MT, WNC), pp. 20–34.
SFMSFM-2014-AmighiBDHMZ #concurrent #verification
Verification of Concurrent Systems with VerCors (AA, SB, SD, MH, WM, MZS), pp. 172–216.
ICFPICFP-2014-NguyenTH #contract #verification
Soft contract verification (PCN, STH, DVH), pp. 139–152.
GT-VMTGT-VMT-2014-WangBL #alloy #graph #model transformation #using #verification
Verification of Graph-based Model Transformations Using Alloy (XW, FB, YL).
ICGTICGT-2014-Delzanno #distributed #model checking #protocol #verification
Parameterized Verification and Model Checking for Distributed Broadcast Protocols (GD), pp. 1–16.
ICGTICGT-2014-SelimLCDO #graph #model transformation #specification #verification
Specification and Verification of Graph-Based Model Transformation Properties (GMKS, LL, JRC, JD, BJO), pp. 113–129.
CHICHI-2014-BurgbacherH #gesture #type system #verification
An implicit author verification system for text messages based on gesture typing biometrics (UB, KHH), pp. 2951–2954.
HCIHIMI-DE-2014-TanikawaSKF #design #problem #process #usability #verification
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.
AdaEuropeAdaEurope-2014-PedroPPP #ada #framework #programming language #runtime #towards #verification
Towards a Runtime Verification Framework for the Ada Programming Language (AdMP, DP, LMP, JSP), pp. 58–73.
HILTHILT-2014-Ball #compilation #correctness #logic #research #verification
Correctness via compilation to logic: a decade of verification at microsoft research (TB), pp. 69–70.
CAiSECAiSE-2014-LaurentBBG #formal method #process #verification
Formalization of fUML: An Application to Process Verification (YL, RB, SB, MPG), pp. 347–363.
ICEISICEIS-v2-2014-AntonioRF #embedded #modelling #process #validation #verification
Verification and Validation Activities for Embedded Systems — A Feasibility Study on a Reading Technique for SysML Models (EAA, RR, SCPFF), pp. 233–240.
CIKMCIKM-2014-YangQ #image #mobile #retrieval #scalability #verification
Spatial Verification for Scalable Mobile Image Retrieval (XY, XQ), pp. 1903–1906.
ICPRICPR-2014-PinheiroRCJS #fuzzy #independence #robust #verification
Type-2 Fuzzy GMMs for Robust Text-Independent Speaker Verification in Noisy Environments (HNBP, TIR, GDCC, IJT, JS), pp. 4531–4536.
ICPRICPR-2014-ZhangWGZZ #analysis #using #verification
Low Computation Face Verification Using Class Center Analysis (XZ, JW, YG, SZ, SZ), pp. 4543–4547.
KRKR-2014-LomuscioM #abstraction #atl #multi #specification #verification
An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications (AL, JM).
SEKESEKE-2014-GuptaAWD #empirical #modelling #verification
Evaluating the Use of Model-Based Requirement Verification Method: An Empirical Study (MG, DA, GSW, HD), pp. 397–401.
SEKESEKE-2014-NguyenC #case study #coordination #requirements #verification
Formal Verification of Coordination Systems’ Requirements — A Case Study on the European Train Control System (HNN, ARC), pp. 393–396.
SIGIRSIGIR-2014-DamH #scalability #topic #verification
Large-scale author verification: temporal and topical influences (MvD, CH), pp. 1039–1042.
ECMFAECMFA-2014-LaurentBBG #alloy #framework #process #verification
Alloy4SPV : A Formal Framework for Software Process Verification (YL, RB, SB, MPG), pp. 83–100.
OnwardOnward-2014-VisserWTNVPK #design #implementation #verification
A Language Designer’s Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs (EV, GW, APT, PN, VAV, AP, GK), pp. 95–111.
OOPSLAOOPSLA-2014-WangCC #abstraction #compilation #verification
Compiler verification meets cross-language linking via data abstraction (PW, SC, AC), pp. 675–690.
LOPSTRLOPSTR-2014-TahatE #hybrid #protocol #self #synthesis #verification
A Hybrid Method for the Verification and Synthesis of Parameterized Self-Stabilizing Protocols (AT, AE), pp. 201–218.
POPLPOPL-2014-BartheFGSSB #encryption #implementation #probability #relational #verification
Probabilistic relational verification for cryptographic implementations (GB, CF, BG, PYS, NS, SZB), pp. 193–206.
POPLPOPL-2014-BurckhardtGYZ #data type #specification #verification
Replicated data types: specification, verification, optimality (SB, AG, HY, MZ), pp. 271–284.
RERE-2014-BadgerTC #analysis #design #named #requirements #verification
VARED: Verification and analysis of requirements and early designs (JMB, DT, CC), pp. 325–326.
RERE-2014-LetychevskyiW #requirements #verification
Symbolic verification of requirements in VRS system (OL, TW), pp. 331–332.
RERE-2014-WittFSH #process #validation #verification
Business Application Modeler: A process model Validation and Verification tool (SW, SF, AS, CH), pp. 333–334.
FSEFSE-2014-Kan #model checking #safety #traceability #verification
Traceability and model checking to support safety requirement verification (SK), pp. 783–786.
FSEFSE-2014-Llerena #nondeterminism #verification
Dealing with uncertainty in verification of nondeterministic systems (YRSL), pp. 787–790.
ICSEICSE-2014-BocicB #induction #invariant #verification #web
Inductive verification of data model invariants for web applications (IB, TB), pp. 620–631.
ICSEICSE-2014-LeP #control flow #graph #interprocedural #multi #verification
Patch verification via multiversion interprocedural control flow graphs (WL, SDP), pp. 1047–1058.
SPLCSPLC-2014-MennickeLSW #automation #feature model #petri net #process #verification #workflow
Automated verification of feature model configuration processes based on workflow Petri nets (SM, ML, JS, TW), pp. 62–71.
SPLCSPLC-2014-SimidchievaO #composition #generative #product line #verification
Generation, composition, and verification of families of human-intensive systems (BIS, LJO), pp. 207–216.
HPCAHPCA-2014-ZhangBES #design #named #protocol #scalability #verification
PVCoherence: Designing flat coherence protocols for scalable verification (MZ, JDB, JE, DJS), pp. 392–403.
OSDIOSDI-2014-HawblitzelHLNPZZ #automation #security #verification
Ironclad Apps: End-to-End Security via Automated Full-System Verification (CH, JH, JRL, AN, BP, DZ, BZ), pp. 165–181.
CAVCAV-2014-AbdullaACHRRS #constraints #string #verification
String Constraints for Verification (PAA, MFA, YFC, LH, AR, PR, JS), pp. 150–166.
CAVCAV-2014-BardsleyBCCDDKLQ #gpu #kernel #verification
Engineering a Static Verification Tool for GPU Kernels (EB, AB, NC, PC, PD, AFD, JK, DL, SQ), pp. 226–242.
CAVCAV-2014-BeyerDW #verification
Software Verification in the Google App-Engine Cloud (DB, GD, PW), pp. 327–333.
CAVCAV-2014-CermakLMM #logic #model checking #named #specification #verification
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PC, AL, FM, AM), pp. 525–532.
CAVCAV-2014-HuangFMMK #automaton #hybrid #invariant #network #verification
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells (ZH, CF, AM, SM, MZK), pp. 373–390.
CAVCAV-2014-LeeS #abstraction #approximate #bound #reachability #scalability #verification
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (SL, KAS), pp. 849–865.
CAVCAV-2014-LesaniMP #automation #concurrent #data type #verification
Automatic Atomicity Verification for Clients of Concurrent Data Structures (ML, TDM, JP), pp. 550–567.
CAVCAV-2014-SanchezS #concurrent #data type #named #verification
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (AS, CS), pp. 620–627.
IJCARIJCAR-2014-Zhang #encoding #verification
QBF Encoding of Temporal Properties and QBF-Based Verification (WZ), pp. 224–239.
ISSTAISSTA-2014-PastoreMHFSSM #testing
Verification-aided regression testing (FP, LM, AEJH, GF, NS, SS, AM), pp. 37–48.
LICSLICS-CSL-2014-LiangFS #composition #concurrent #refinement #source code #verification
Compositional verification of termination-preserving refinement of concurrent programs (HL, XF, ZS), p. 10.
SMTSMT-2014-Melquiond #algorithm #automation #float #verification
Automating the Verification of Floating-Point Algorithms (GM), p. 63.
TAPTAP-2014-DiepenbeckKSD #behaviour #development #testing #verification
Behaviour Driven Development for Tests and Verification (MD, UK, MS, RD), pp. 61–77.
TAPTAP-2014-HilkenNGW #behaviour #comparison #modelling #ocl #uml #verification
Filmstripping and Unrolling: A Comparison of Verification Approaches for UML and OCL Behavioral Models (FH, PN, MG, RW), pp. 99–116.
TAPTAP-2014-KampmannGZ #bound #execution #named #performance #verification
JTACO: Test Execution for Faster Bounded Verification (AK, JPG, AZ), pp. 134–141.
TAPTAP-2014-KanigCCGMR #verification
Explicit Assumptions — A Prenup for Marrying Static and Dynamic Program Verification (JK, RC, CC, JG, YM, ER), pp. 142–157.
TAPTAP-2014-KosmatovLA #case study #proving #testing #verification
A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing (NK, ML, CA), pp. 158–164.
TAPTAP-2014-PetiotKGJ #deduction #generative #how #specification #testing #verification
How Test Generation Helps Software Specification and Deductive Verification in Frama-C (GP, NK, AG, JJ), pp. 204–211.
VMCAIVMCAI-2014-AngelisFPP #array #source code #verification
Verifying Array Programs by Transforming Verification Conditions (EDA, FF, AP, MP), pp. 182–202.
VMCAIVMCAI-2014-JezequelE #algorithm #distributed #message passing #protocol #verification
Message-Passing Algorithms for the Verification of Distributed Protocols (LJ, JE), pp. 222–241.
CBSECBSE-2013-BarnatBCP #component #named #verification
DCCL: verification of component systems with ensembles (JB, NB, IC, ZP), pp. 43–52.
CBSECBSE-2013-JohnsonCK #component #framework #incremental #verification
An incremental verification framework for component-based software systems (KJ, RC, SK), pp. 33–42.
ASEASE-2013-0002IP #c #concurrent #named #preprocessor #tool support #verification
CSeq: A concurrency pre-processor for sequential C verification tools (BF, OI, GP), pp. 710–713.
ASEASE-2013-DhunganaTWW #automation #interactive #rule-based #verification
Automated verification of interactive rule-based configuration systems (DD, CHT, CW, PW), pp. 551–561.
ASEASE-2013-Frank #automation #challenge #validation #verification
The challenges of verification and validation of automated planning systems (keynote) (JF), p. 2.
ASEASE-2013-MaezawaWTH #ajax #automation #interactive #invariant #verification
Automated verification of pattern-based interaction invariants in Ajax applications (YM, HW, YT, SH), pp. 158–168.
ASEASE-2013-MeredithR #parametricity #performance #runtime #string #verification
Efficient parametric runtime verification with deterministic string rewriting (POM, GR), pp. 70–80.
CASECASE-2013-MohajeraniMF #automaton #composition #finite #using #verification
Compositional nonblocking verification for extended finite-state automata using partial unfolding (SM, RM, MF), pp. 930–935.
DACDAC-2013-ChenWBA #random #reuse #simulation #verification
Simulation knowledge extraction and reuse in constrained random processor verification (WC, LCW, JB, MSA), p. 6.
DACDAC-2013-Feng #grid #power management #scalability #verification
Scalable vectorless power grid current integrity verification (ZF), p. 8.
DACDAC-2013-GoswamiLKSMCR #development #modelling #verification
Model-based development and verification of control software for electric vehicles (DG, ML, MK, SS, AM, SC, SR), p. 9.
DACDAC-2013-LeGHD #simulation #using #verification
Verifying SystemC using an intermediate verification language and symbolic simulation (HML, DG, VH, RD), p. 6.
DACDAC-2013-LinLM #analysis #hybrid #kernel #reachability #verification
Verification of digitally-intensive analog circuits via kernel ridge regression and hybrid reachability analysis (HL, PL, CJM), p. 6.
DACDAC-2013-WuH #constraints #framework #multi #random #robust #set #theorem proving #verification
A robust constraint solving framework for multiple constraint sets in constrained random verification (BHW, CY(H), p. 7.
DACDAC-2013-XiongW #abstraction #constraints #grid #power management #verification
Constraint abstraction for vectorless power grid verification (XX, JW), p. 6.
DACDAC-2013-ZhangYWSX #hardware #named #trust #verification
VeriTrust: verification for hardware trust (JZ, FY, LW, ZS, QX), p. 8.
DATEDATE-2013-AhmadyanKV #algorithm #incremental #runtime #using #verification
Runtime verification of nonlinear analog circuits using incremental time-augmented RRT algorithm (SNA, JAK, SV), pp. 21–26.
DATEDATE-2013-FreitasRS #concurrent #consistency #memory management #on the fly #verification
On-the-fly verification of memory consistency with concurrent relaxed scoreboards (LSF, EAR, LCVdS), pp. 631–636.
DATEDATE-2013-MillerB #parametricity #satisfiability #verification
Formal verification of analog circuit parameters across variation utilizing SAT (MM, FB), pp. 1442–1447.
DATEDATE-2013-SeiterWSD #ocl #specification #uml #verification
Determining relevant model elements for the verification of UML/OCL specifications (JS, RW, MS, RD), pp. 1189–1192.
DATEDATE-2013-WilleGSKD #modelling #towards #verification
Towards a generic verification methodology for system models (RW, MG, MS, MK, RD), pp. 1193–1196.
DRRDRR-2013-RicquebourgCG #evaluation #recognition #robust #verification #word
Evaluation of lexicon size variations on a verification and rejection system based on SVM, for accurate and robust recognition of handwritten words (YR, BC, LG).
DRRDRR-2013-SrihariKTB #using #verification
Combining evidence using likelihood ratios in writer verification (SNS, DK, YT, GRB).
ICDARICDAR-2013-HuC #classification #pseudo #using #verification
Offline Signature Verification Using Real Adaboost Classifier Combination of Pseudo-dynamic Features (JH, YC), pp. 1345–1349.
ICDARICDAR-2013-JainD #detection #documentation #image #named #verification
VisualDiff: Document Image Verification and Change Detection (RJ, DSD), pp. 40–44.
ICDARICDAR-2013-KamihiraOWK #verification
Improvement of Japanese Signature Verification by Segmentation-Verification (YK, WO, TW, FK), pp. 379–382.
ICDARICDAR-2013-KhanKS #identification #problem #question #verification
Can Signature Biometrics Address Both Identification and Verification Problems? (SHK, ZK, FS), pp. 981–985.
ICDARICDAR-2013-KhayyatLS #classification #verification #word
Verification of Hierarchical Classifier Results for Handwritten Arabic Word Spotting (MK, LL, CYS), pp. 572–576.
ICDARICDAR-2013-LiPXW #analysis #consistency #online #order #verification
A Stroke Order Verification Method for On-Line Handwritten Chinese Characters Based on Tempo-spatial Consistency Analysis (RL, LP, EX, NW), pp. 999–1003.
ICDARICDAR-2013-MalikALD #forensics #realtime #verification
FREAK for Real Time Forensic Signature Verification (MIM, SA, ML, AD), pp. 971–975.
ICDARICDAR-2013-MalikLAOBF #contest #identification #verification
ICDAR 2013 Competitions on Signature Verification and Writer Identification for On- and Offline Skilled Forgeries (SigWiComp 2013) (MIM, ML, LA, WO, MB, BF), pp. 1477–1483.
ICDARICDAR-2013-MalikLD #automation #comparison #forensics #verification
Part-Based Automatic System in Comparison to Human Experts for Forensic Signature Verification (MIM, ML, AD), pp. 872–876.
PODSPODS-2013-BojanczykST #verification
Verification of database-driven systems via amalgamation (MB, LS, ST), pp. 63–74.
PODSPODS-2013-HaririCGDM #relational #verification
Verification of relational data-centric dynamic systems with external services (BBH, DC, GDG, AD, MM), pp. 163–174.
ESOPESOP-2013-AlglaveKNT #memory management #program transformation #verification
Software Verification for Weak Memory via Program Transformation (JA, DK, VN, MT), pp. 512–532.
ESOPESOP-2013-CollingbourneDKQ #analysis #gpu #kernel #semantics #verification
Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels (PC, AFD, JK, SQ), pp. 270–289.
ESOPESOP-2013-KassiosK #verification
A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness (ITK, EK), pp. 149–168.
FoSSaCSFoSSaCS-2013-MioS #composition #concurrent #probability #process #proving #verification
A Proof System for Compositional Verification of Probabilistic Concurrent Processes (MM, AS), pp. 161–176.
TACASTACAS-2013-AbdullaHHJR #concurrent #data type #specification #verification
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures (PAA, FH, LH, BJ, AR), pp. 324–338.
TACASTACAS-2013-AlbarghouthiGLCC #abstract interpretation #contest #named #verification
UFO: Verification with Interpolants and Abstract Interpretation — (Competition Contribution) (AA, AG, YL, SC, MC), pp. 637–640.
TACASTACAS-2013-Beyer #contest #summary #verification
Second Competition on Software Verification — (Summary of SV-COMP 2013) (DB0), pp. 594–609.
TACASTACAS-2013-DudkaMPV #contest #low level #named #verification
Predator: A Tool for Verification of Low-Level List Manipulation — (Competition Contribution) (KD, PM, PP, TV), pp. 627–629.
TACASTACAS-2013-GrigoreDPT #automaton #runtime #verification
Runtime Verification Based on Register Automata (RG, DD, RLP, NT), pp. 260–276.
TACASTACAS-2013-LindenW #approach #memory management
A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems (AL, PW), pp. 339–353.
PLDIPLDI-2013-LiangF #composition #verification
Modular verification of linearizability with non-fixed linearization points (HL, XF), pp. 459–470.
PLDIPLDI-2013-ZhaoNMZ #optimisation #verification
Formal verification of SSA-based optimizations for LLVM (JZ, SN, MMKM, SZ), pp. 175–186.
SASSAS-2013-0001GHAN #concept #geometry #learning #verification
Verification as Learning Geometric Concepts (RS, SG, BH, AA, AVN), pp. 388–411.
SASSAS-2013-BlazyLMP #abstract interpretation #analysis #c #verification
Formal Verification of a C Value Analysis Based on Abstract Interpretation (SB, VL, AM, DP), pp. 324–344.
SASSAS-2013-BrainDGHK #float #source code #verification
Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL (MB, VD, AG, LH, DK), pp. 412–432.
SASSAS-2013-DOsualdoKO #automation #concurrent #verification
Automatic Verification of Erlang-Style Concurrency (ED, JK, CHLO), pp. 454–476.
SASSAS-2013-DudkaPV #low level #verification
Byte-Precise Verification of Low-Level List Manipulation (KD, PP, TV), pp. 215–237.
SASSAS-2013-MajumdarMW #message passing #source code #verification
Static Provenance Verification for Message Passing Programs (RM, RM, ZW), pp. 366–387.
LATALATA-2013-DelzannoT #complexity #decidability #network #verification
Decidability and Complexity Results for Verification of Asynchronous Broadcast Networks (GD, RT), pp. 238–249.
IFMIFM-2013-GavaFG #algorithm #deduction #verification
Deductive Verification of State-Space Algorithms (FG, JF, MG), pp. 124–138.
IFMIFM-2013-IshiiMN #automaton #calculus #hybrid #induction #verification
Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus (DI, GM, SN), pp. 139–153.
IFMIFM-2013-MeryP #formal method #modelling #protocol #verification
Formal Modelling and Verification of Population Protocols (DM, MP), pp. 208–222.
IFMIFM-2013-MilloRKN #composition #product line #verification
Compositional Verification of Software Product Lines (JVM, SR, SNK, GKN), pp. 109–123.
IFMIFM-2013-MoranHS #automation #verification
Automated Anonymity Verification of the ThreeBallot Voting System (MM, JH, SS), pp. 94–108.
IFMIFM-2013-VekrisLDM #specification #using #verification
Verification of EB3 Specifications Using CADP (DV, FL, CD, RM), pp. 61–76.
SEFMSEFM-2013-BoerGW #runtime #verification
Run-Time Verification of Coboxes (FSdB, SdG, PYHW), pp. 259–273.
SEFMSEFM-2013-GesellMS #verification
Lifting Verification Results for Preemption Statements (MG, AM, KS), pp. 91–105.
SEFMSEFM-2013-Klimek #logic #modelling #requirements #specification #verification
From Extraction of Logical Specifications to Deduction-Based Formal Verification of Requirements Models (RK), pp. 61–75.
SEFMSEFM-2013-PerceboisST #graph transformation #invariant #transitive #verification
Rule-Level Verification of Graph Transformations for Invariants Based on Edges’ Transitive Closure (CP, MS, HNT), pp. 106–121.
ICFPICFP-2013-BroadbentCHS #approach #higher-order #named #verification
C-SHORe: a collapsible approach to higher-order verification (CHB, AC, MH, OS), pp. 13–24.
ICFPICFP-2013-LorenzenE #automation #composition #verification
Modular and automated type-soundness verification for language extensions (FL, SE), pp. 331–342.
IFLIFL-2013-GijzelN #framework #implementation #modelling #towards #verification
Towards a framework for the implementation and verification of translations between argumentation models (BvG, HN), p. 93.
HCIDHM-HB-2013-XieKD #modelling #verification
Anatomy-Based Variational Modeling of Digital Hand and Its Verification (YX, SK, HD), pp. 384–392.
HILTHILT-2013-Alagic #automation #interactive #verification
Automatic versus interactive program verification (SA), pp. 87–88.
HILTHILT-2013-EfstathopoulosH #optimisation #verification
Optimizing verification effort with SPARK 2014 (PE, AH), pp. 19–20.
HILTHILT-2013-Logozzo #contract #specification #verification
Practical specification and verification with code contracts (FL), pp. 7–8.
HILTHILT-2013-MurugesanWRH #composition #verification
Compositional verification of a medical device system (AM, MWW, SR, MPEH), pp. 51–64.
EDOCEDOC-2013-TranZ #analysis #approach #architecture #verification
Event Actors Based Approach for Supporting Analysis and Verification of Event-Driven Architectures (HT, UZ), pp. 217–226.
MODELSMoDELS-2013-PiresPWD #behaviour #embedded #source code #verification
Behavioural Verification in Embedded Software, from Model to Source Code (AFP, TP, VW, SD), pp. 320–335.
MODELSMoDELS-2013-SelimBCDW #automation #industrial #model transformation #verification
Automated Verification of Model Transformations in the Automotive Industry (GMKS, FB, JRC, JD, SW), pp. 690–706.
MODELSMoDELS-2013-ZalilaCP #approach #domain-specific language #integration #verification
Formal Verification Integration Approach for DSML (FZ, XC, MP), pp. 336–351.
MODELSMoDELS-2013-PiresPWD #behaviour #embedded #source code #verification
Behavioural Verification in Embedded Software, from Model to Source Code (AFP, TP, VW, SD), pp. 320–335.
MODELSMoDELS-2013-SelimBCDW #automation #industrial #model transformation #verification
Automated Verification of Model Transformations in the Automotive Industry (GMKS, FB, JRC, JD, SW), pp. 690–706.
MODELSMoDELS-2013-ZalilaCP #approach #domain-specific language #integration #verification
Formal Verification Integration Approach for DSML (FZ, XC, MP), pp. 336–351.
ECOOPECOOP-2013-HeuleKMS #abstraction #generative #logic #verification
Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions (SH, ITK, PM, AJS), pp. 451–476.
LOPSTRLOPSTR-2013-Vidal #erlang #term rewriting #towards #verification
Towards Erlang Verification by Term Rewriting (GV), pp. 109–126.
POPLPOPL-2013-UnnoTK #automation #functional #higher-order #source code #verification
Automating relatively complete verification of higher-order functional programs (HU, TT, NK), pp. 75–86.
RERE-2013-GhezziMSS #on the #requirements #verification
On requirements verification for model refinements (CG, CM, AMS, PS), pp. 62–71.
SACSAC-2013-CogniniFPPR #collaboration #modelling #named #process #verification
HawkEye: a tool for collaborative business process modelling and verification (RC, DF, AP, AP, BR), pp. 785–786.
ESEC-FSEESEC-FSE-2013-BeyerLNSW #performance #precise #reuse #verification
Precision reuse for efficient regression verification (DB, SL, EN, AS, PW), pp. 389–399.
ESEC-FSEESEC-FSE-2013-NavabpourJWBMBF #c #named #runtime #source code #verification
RiTHM: a tool for enabling time-triggered runtime verification for C programs (SN, YJ, CWWW, SB, RM, BB, SF), pp. 603–606.
ESEC-FSEESEC-FSE-2013-ZervoudakisREF #model checking #verification
Cascading verification: an integrated method for domain-specific model checking (FZ, DSR, SGE, AF), pp. 400–410.
ICSEICSE-2013-ApelRWGB #case study #product line #verification
Strategies for product-line verification: case studies and experiments (SA, AvR, PW, AG, DB), pp. 482–491.
ICSEICSE-2013-BohmeOR #verification
Partition-based regression verification (MB, BCdSO, AR), pp. 302–311.
ICSEICSE-2013-HatcliffRCB #execution #framework #symbolic computation #verification
Explicating symbolic execution (xSymExe): an evidence-based verification framework (JH, R, PC, JB), pp. 222–231.
SLESLE-2013-PearceG #framework #named #research #verification
Whiley: A Platform for Research in Software Verification (DJP, LG), pp. 238–248.
HPCAHPCA-2013-BeuPHC #performance #verification
High-speed formal verification of heterogeneous coherence hierarchies (JGB, JAP, ERH, TMC), pp. 566–577.
PLOSPLOS-2013-KellerMAOCRKH #exclamation #file system #verification
File systems deserve verification too! (GK, TCM, SA, LO, ZC, LR, GK, GH), p. 7.
PPoPPPPoPP-2013-BartheCKGM #relational #synthesis #verification
From relational verification to SIMD loop synthesis (GB, JMC, SG, CK, MM), pp. 123–134.
CADECADE-2013-HahnleSB #reuse #verification
Reuse in Software Verification by Abstract Method Calls (RH, IS, RB), pp. 300–314.
CADECADE-2013-Sofronie-Stokkermans #generative #hybrid #parametricity #reasoning #verification
Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems (VSS), pp. 360–376.
CAVCAV-2013-BraibantC #hardware #synthesis #verification
Formal Verification of Hardware Synthesis (TB, AC), pp. 213–228.
CAVCAV-2013-EsparzaGM #verification
Parameterized Verification of Asynchronous Shared-Memory Systems (JE, PG, RM), pp. 124–140.
CAVCAV-2013-KongHSHG #generative #hybrid #safety #verification
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems (HK, FH, XS, WNNH, MG), pp. 242–257.
CAVCAV-2013-ManciniMMMMT #model checking #simulation #verification
System Level Formal Verification via Model Checking Driven Simulation (TM, FM, AM, IM, FM, ET), pp. 296–312.
CAVCAV-2013-PuggelliLSS #nondeterminism #polynomial #verification
Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties (AP, WL, ALSV, SAS), pp. 527–542.
CAVCAV-2013-RummerHK #verification
Disjunctive Interpolants for Horn-Clause Verification (PR, HH, VK), pp. 347–363.
ICLPICLP-J-2013-GiordanoMSD #constraints #process #programming #set #verification
Business process verification with constraint temporal answer set programming (LG, AM, MS, DTD), pp. 641–655.
ICSTICST-2013-KangKHKNSC #formal method #modelling #verification
Formal Modeling and Verification of SDN-OpenFlow (MK, EYEK, DYH, BJK, KHN, MKS, JYC), pp. 481–482.
ISSTAISSTA-2013-Thum #contract #feature model #product line #verification
Product-line verification with feature-oriented contracts (TT), pp. 374–377.
TAPTAP-2013-ArthoBS #modelling #testing #verification
Model-Based Testing for Verification Back-Ends (CA, AB, MS), pp. 39–55.
TAPTAP-2013-BeckertB0 #metric #testing #verification
A Metric for Testing Program Verification Systems (BB, TB, MW), pp. 56–75.
ASEASE-2012-BiallasBK #framework #logic #programmable #verification
Arcade.PLC: a verification platform for programmable logic controllers (SB, JB, SK), pp. 338–341.
ASEASE-2012-Gabmeyer #model transformation #verification
Formal verification techniques for model transformations specified by-demonstration (SG), pp. 390–393.
ASEASE-2012-NijjarB #bound #smt #using #verification
Unbounded data model verification using SMT solvers (JN, TB), pp. 210–219.
CASECASE-2012-KlotzSSFTS #on the #verification
On the formal verification of routing in material handling systems (TK, NS, BS, EF, KT, JS), pp. 8–13.
CASECASE-2012-WimbockRC #coordination #verification
Derivation and verification of synergy coordinates for the DLR hand arm system (TW, JR, MC), pp. 454–460.
DACDAC-2012-AbhishekN #grid #incremental #power management #verification
Incremental power grid verification (A, FNN), pp. 151–156.
DACDAC-2012-KumarGCALT #approach #cyber-physical #hybrid #verification
A hybrid approach to cyber-physical systems verification (PK, DG, SC, AA, KL, LT), pp. 688–696.
DACDAC-2012-LiSJ #crowdsourcing #named #towards #verification
CrowdMine: towards crowdsourced human-assisted verification (WL, SAS, SJ), pp. 1254–1255.
DACDAC-2012-Seshia #deduction #induction #named #synthesis #verification
Sciduction: combining induction, deduction, and structure for verification and synthesis (SAS), pp. 356–365.
DACDAC-2012-UrdahlSWK #abstraction #composition #concurrent #verification
System verification of concurrent RTL modules by compositional path predicate abstraction (JU, DS, MW, WK), pp. 334–343.
DATEDATE-2012-Al-HashimiM #framework #hardware #question #verification
Accelerators and emulators: Can they become the platform of choice for hardware verification? (BMAH, RM), p. 430.
DATEDATE-2012-BeckerDFMPV #embedded #evolution #modelling #named #scalability #verification
MOUSSE: Scaling modelling and verification to complex Heterogeneous Embedded Systems evolution (MB, GBD, FF, WM, GP, SV), pp. 296–299.
DATEDATE-2012-BombieriFG #fault #framework #functional #named #simulation #verification
FAST-GP: An RTL functional verification framework based on fault simulation on GP-GPUs (NB, FF, VG), pp. 562–565.
DATEDATE-2012-DenizSH #embedded #manycore #verification
Verification coverage of embedded multicore applications (ED, AS, JH), pp. 252–255.
DATEDATE-2012-GuglielmoGFP #design #embedded #modelling #verification
Enabling dynamic assertion-based verification of embedded software through model-driven design (GDG, LDG, FF, GP), pp. 212–217.
DATEDATE-2012-HaedickeGD #metric #verification
A guiding coverage metric for formal verification (FH, DG, RD), pp. 617–622.
DATEDATE-2012-HammamiLB #named #network #verification
NOCEVE: Network on chip emulation and verification environment (OH, XL, JMB), pp. 163–164.
DATEDATE-2012-JongheMGMTS #modelling #roadmap #testing #verification
Advances in variation-aware modeling, verification, and testing of analog ICs (DdJ, EM, GGEG, TM, BT, HGDS), pp. 1615–1620.
DATEDATE-2012-LvKE #multi #performance #reduction #verification
Efficient Gröbner basis reductions for formal verification of galois field multipliers (JL, PK, FE), pp. 899–904.
DATEDATE-2012-MarinMLB #design #incremental #using #verification
Verification of partial designs using incremental QBF solving (PM, CM, MDTL, BB), pp. 623–628.
DATEDATE-2012-RamboHS #consistency #memory management #multi #on the #verification
On ESL verification of memory consistency for system-on-chip multiprocessing (EAR, OPH, LCVdS), pp. 9–14.
DATEDATE-2012-RayB #scalability #verification
Scalable progress verification in credit-based flow-control systems (SR, RKB), pp. 905–910.
DATEDATE-2012-YordanovAGGCBHBD #biology #verification
Experimentally driven verification of synthetic biological circuits (BY, EA, RG, EAG, SBC, SB, TH, CB, DD), pp. 236–241.
DRRDRR-2012-CoetzerSS #collaboration #human-computer #performance #verification
Efficient cost-sensitive human-machine collaboration for offline signature verification (JC, JPS, RS).
DRRDRR-2012-NagyT #named #performance #verification
VeriClick: an efficient tool for table format verification (GN, MT).
VLDBVLDB-2012-GoodrichNOPTTL #authentication #crawling #performance #verification #web
Efficient Verification of Web-Content Searching Through Authenticated Web Crawlers (MTG, DN, OO, CP, RT, NT, CVL), pp. 920–931.
CSEETCSEET-2012-Virseda #algebra #data type #implementation #specification #testing #verification
A Software Testing Tool for the Verification of Abstract Data Type Implementations from Formal Algebraic Specifications (RdVV), pp. 100–104.
ESOPESOP-2012-ChadhaCK #automation #encryption #equivalence #protocol #verification
Automated Verification of Equivalence Properties of Cryptographic Protocols (RC, SC, SK), pp. 108–127.
TACASTACAS-2012-Beyer #contest #verification
Competition on Software Verification — (SV-COMP) (DB0), pp. 504–524.
TACASTACAS-2012-ChenFKPS #automation #probability #verification
Automatic Verification of Competitive Stochastic Systems (TC, VF, MZK, DP, AS), pp. 315–330.
TACASTACAS-2012-CoxSC #bound #precise #verification
A Bit Too Precise? Bounded Verification of Quantized Digital Filters (AC, SS, BYEC), pp. 33–47.
TACASTACAS-2012-DudkaMPV #contest #data type #linked data #named #open data #source code #verification
Predator: A Verification Tool for Programs with Dynamic Linked Data Structures — (Competition Contribution) (KD, PM, PP, TV), pp. 545–548.
TACASTACAS-2012-HardinSWP #verification
The Guardol Language and Verification System (DSH, KS, MWW, THP), pp. 18–32.
TACASTACAS-2012-HeussnerGS #communication #framework #named #verification
McScM: A General Framework for the Verification of Communicating Machines (AH, TLG, GS), pp. 478–484.
TACASTACAS-2012-JiangPMAM #modelling #verification
Modeling and Verification of a Dual Chamber Implantable Pacemaker (ZJ, MP, SM, RA, RM), pp. 188–203.
TACASTACAS-2012-YehWH #design #framework #named #open source #synthesis #towards #verification
QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification (HHY, CYW, CY(H), pp. 377–391.
CSMRCSMR-2012-CastrejonLV #architecture #maintenance #named #verification #web
Web2MexADL: Discovery and Maintainability Verification of Software Systems Architecture (JCC, RL, GVS), pp. 531–534.
MSRMSR-2012-SouzaC #debugging #ide #open source #verification
Characterizing verification of bug fixes in two open source IDEs (RS, CC), pp. 70–73.
PEPMPEPM-2012-Berger #metaprogramming #specification #verification
Specification and verification of meta-programs (MB), pp. 3–4.
FLOPSFLOPS-2012-Terauchi #automation #functional #higher-order #source code #verification
Automated Verification of Higher-Order Functional Programs (TT), p. 2.
FMFM-2012-ChristakisMW #collaboration #testing #verification
Collaborative Verification and Testing with Explicit Assumptions (MC, PM, VW), pp. 132–146.
FMFM-2012-HojjatKGIKR #tool support #verification
A Verification Toolkit for Numerical Transition Systems — Tool Paper (HH, FK, FG, RI, VK, PR), pp. 247–251.
FMFM-2012-JohnsonGMDE #case study #hybrid #verification
Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems (TTJ, JG, SM, RD, RSE), pp. 252–266.
FMFM-2012-LinLSDA #automation #composition #verification
Automatic Compositional Verification of Timed Systems (SWL, YL, JS, JSD, ÉA), pp. 272–276.
IFMIFM-2012-BlackmoreHBER #automation #generative #simulation #verification
Analysing and Closing Simulation Coverage by Automatic Generation and Verification of Formal Properties from Coverage Reports (TB, DH, PB, KE, NR), pp. 84–98.
IFMIFM-2012-CalderS #algebra #case study #network #process #runtime #verification
Process Algebra for Event-Driven Runtime Verification: A Case Study of Wireless Network Management (MC, MS), pp. 21–23.
IFMIFM-2012-NgoTGGB #compilation #equation #verification
Formal Verification of Compiler Transformations on Polychronous Equations (VCN, JPT, TG, PLG, LB), pp. 113–127.
IFMIFM-2012-RochaCMS #execution #interactive #verification
A Formal Interactive Verification Environment for the Plan Execution Interchange Language (CR, HC, CAM, RS), pp. 343–357.
IFMIFM-2012-TarasyukTL #formal method #modelling #probability #verification
Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B (AT, ET, LL), pp. 237–252.
SEFMSEFM-2012-BicknellRBCS #approach #using #verification
A Practical Approach for Closed Systems Formal Verification Using Event-B (BB, JR, MJB, JC, CFS), pp. 323–332.
SEFMSEFM-2012-ColomboFMP #bound #configuration management #monitoring #named #resource management #runtime #verification
polyLarva: Runtime Verification with Configurable Resource-Aware Monitoring Boundaries (CC, AF, RM, GJP), pp. 218–232.
SEFMSEFM-2012-PaulSS #assembly #automation #verification
Completing the Automated Verification of a Small Hypervisor — Assembler Code Verification (WJP, SS, AS), pp. 188–202.
SEFMSEFM-2012-ZhangKJ #composition #verification
Verification of Aspectual Composition in Feature-Modeling (QZ, RK, JJ), pp. 109–125.
ICFPICFP-2012-Huffman #monad #verification
Formal verification of monad transformers (BH), pp. 15–16.
ICGTICGT-2012-GieseL #automation #behaviour #invariant #model transformation #towards #verification
Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking (HG, LL), pp. 249–263.
ICGTICGT-2012-Poskitt #graph #source code #verification
Verification of Graph Programs (CMP), pp. 420–422.
ICGTICGT-2012-Vandin #specification #verification
Specification and Verification of Modal Properties for Structured Systems (AV), pp. 423–425.
HILTHILT-2012-BeltCHR #ada #automation #contract #using #verification
Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan (JB, PC, JH, R), pp. 3–4.
HILTHILT-2012-Kanig #ada #testing #verification
Leading-edge ada verification technologies: combining testing and verification with GNATTest and GNATProve — the hi-lite project (JK), pp. 5–6.
HILTHILT-2012-KanigSD #compilation #convergence #named #verification
Hi-Lite: the convergence of compiler technology and program verification (JK, ES, CD), pp. 27–34.
HILTHILT-2012-Leino12a #proving #using #verification #why
Program proving using intermediate verification languages (IVLs) like boogie and why3 (KRML), pp. 25–26.
CAiSECAiSE-2012-Razo-ZapataLGA #fuzzy #network #verification
Fuzzy Verification of Service Value Networks (ISRZ, PDL, JG, HA), pp. 95–110.
ICEISICEIS-v2-2012-CapelM #approach #automation #composition #correctness #model checking #safety #verification
A Formal Compositional Verification Approach for Safety-Critical Systems Correctness — Model-Checking based Methodological Approach to Automatically Verify Safety Critical Systems Software (MIC, LEMM), pp. 105–112.
ICPRICPR-2012-KennardBS #2d #approach #detection #geometry #using #verification
Offline signature verification and forgery detection using a 2-D geometric warping approach (DJK, WAB, TWS), pp. 3733–3736.
ICPRICPR-2012-MaoYLZ #classification #invariant #verification
Age-invariant face verification based on Local Classifier Ensemble (XJM, YBY, NL, YZ), pp. 2408–2411.
ICPRICPR-2012-NgC #using #verification
Face verification using temporal affective cues (ESN, AYSC), pp. 1249–1252.
ICPRICPR-2012-StrucZP #normalisation #parametricity #verification
Non-parametric score normalization for biometric verification systems (VS, JZG, NP), pp. 2395–2399.
ICPRICPR-2012-XiaSF #towards #using #verification #visual notation
Toward kinship verification using visual attributes (SX, MS, YF), pp. 549–552.
KRKR-2012-BelardinelliLP #abstraction #verification
An Abstraction Technique for the Verification of Artifact-Centric Systems (FB, AL, FP).
KRKR-2012-GiacomoLP #bound #calculus #decidability #verification
Bounded Situation Calculus Action Theories and Decidable Verification (GDG, YL, FP).
KRKR-2012-HaufeT #automation #game studies #verification
Automated Verification of Epistemic Properties for General Game Playing (SH, MT).
SEKESEKE-2012-BouchenebB #parametricity #verification #workflow
Parametric Verification of TimeWorkflow Nets (HB, KB), pp. 375–380.
SEKESEKE-2012-DuttaUA #analysis #approach #automation #semantics #verification
Requirement Analysis and Automated Verification: A Semantic Approach (AD, PDU, SA), pp. 51–54.
SEKESEKE-2012-LiLCZJZ #adaptation #continuation #self #verification
A HybridUML and QdL Based Verification Method for CPS Self-Adaptability (JL, BL, QC, MZ, SJ, XZ), pp. 239–242.
SEKESEKE-2012-ShenHTGZ #feature model #logic #modelling #verification
Feature modeling and Verification based on Description Logics (GS, ZH, CT, QG, WZ), pp. 422–425.
SEKESEKE-2012-ZhaiLZLCJ #algebra #cyber-physical #logic #verification
Verification of Cyber-Physical Systems Based on Differential-Algebraic Temporal Dynamic Logic (XZ, BL, MZ, JL, QC, SJ), pp. 231–234.
SEKESEKE-2012-ZhuLLCZJ #continuation #difference #logic #using #verification
HybridUML Based Verification of CPS Using Differential Dynamic Logic (MZ, BL, JL, QC, XZ, SJ), pp. 235–238.
ECMFAECMFA-2012-GeP #framework #realtime #safety #uml #verification
Time Properties Verification Framework for UML-MARTE Safety Critical Real-Time Systems (NG, MP), pp. 352–367.
ECMFAECMFA-2012-RadjenovicMPRMBK #automation #embedded #modelling #named #uml #verification
MADES: A Tool Chain for Automated Verification of UML Models of Embedded Systems (AR, NDM, RFP, MR, AM, LB, DSK), pp. 340–351.
ECOOPECOOP-2012-DiasDSL #java #memory management #source code #transaction #verification
Verification of Snapshot Isolation in Transactional Memory Java Programs (RJD, DD, JCS, JL), pp. 640–664.
TOOLSTOOLS-EUROPE-2012-MehnertA #type system #using #verification
Verification of Snapshotable Trees Using Access Permissions and Typestate (HM, JA), pp. 187–201.
GPCEGPCE-2012-ThumSHA #deduction #product line #verification
Family-based deductive verification of software product lines (TT, IS, MH, SA), pp. 11–20.
LOPSTRLOPSTR-2012-SeghirB #array #program transformation #quantifier #verification
Simplifying the Verification of Quantified Array Assertions via Code Transformation (MNS, MB), pp. 194–212.
PPDPPPDP-2012-OlartePRC #approach #automation #concurrent #constraints #linear #verification
A linear concurrent constraint approach for the automatic verification of access permissions (CO, EP, CR, NC), pp. 207–216.
QAPLQAPL-2012-BelardinelliGL #automation #protocol #quantum #using #verification
Automated Verification of Quantum Protocols using MCMAS (FB, PG, AL), pp. 48–62.
POPLPOPL-2012-FarzanK #composition #concurrent #reasoning #source code #verification
Verification of parameterized concurrent programs by modular reasoning about data and control (AF, ZK), pp. 297–308.
SACSAC-2012-AtifMO #detection #verification
Formal verification of Unreliable Failure Detectors in Partially Synchronous Systems (MA, MRM, AO), pp. 478–485.
SACSAC-2012-ChebaroKGJ #dynamic analysis #slicing #verification
Program slicing enhances a verification technique combining static and dynamic analysis (OC, NK, AG, JJ), pp. 1284–1291.
SACSAC-2012-CruzFP #source code #verification
Verification conditions for single-assignment programs (DCdC, MJF, JSP), pp. 1264–1270.
SACSAC-2012-LassaigneP #approximate #markov #process #scalability #verification
Approximate planning and verification for large markov decision processes (RL, SP), pp. 1314–1319.
SACSAC-2012-SalaunEPBC #distributed #in the cloud #protocol #self #verification
Verification of a self-configuration protocol for distributed applications in the cloud (GS, XE, NDP, FB, TC), pp. 1278–1283.
FSEFSE-2012-NearJ #bound #named #verification #web
Rubicon: bounded verification of web applications (JPN, DJ), p. 60.
FSEFSE-2012-ShaikhW #diagrams #ocl #performance #slicing #uml #verification
UMLtoCSP (UOST): a tool for efficient verification of UML/OCL class diagrams through model slicing (AS, UKW), p. 37.
ICSEICSE-2012-AndronickJKKSZZ #perspective #process #scalability #verification
Large-scale formal verification in practice: A process perspective (JA, DRJ, GK, RK, MS, HZ, LZ), pp. 1002–1011.
ICSEICSE-2012-CookHSS #compilation #composition #specification #using #verification
Specification engineering and modular verification using a web-integrated verifying compiler (CTC, HKH, HS, MS), pp. 1379–1382.
ICSEICSE-2012-Motta #modelling #multi #towards #uml #verification
Towards the verification of multi-diagram UML models (AM), pp. 1531–1534.
SPLCSPLC-2012-CordySHL #behaviour #modelling #product line #realtime #verification
Behavioural modelling and verification of real-time software product lines (MC, PYS, PH, AL), pp. 66–75.
PPoPPPPoPP-2012-LiLSGGR #generative #named #testing #verification
GKLEE: concolic verification and test generation for GPUs (GL, PL, GS, GG, IG, SPR), pp. 215–224.
PPoPPPPoPP-2012-MalkisB #verification
Verification of software barriers (AM, AB), pp. 313–314.
CAVCAV-2012-AlbarghouthiLGC #framework #named #verification
Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification (AA, YL, AG, MC), pp. 672–678.
CAVCAV-2012-Bradley #incremental #induction #verification
IC3 and beyond: Incremental, Inductive Verification (ARB), p. 4.
CAVCAV-2012-ChuJ #reduction #safety #symmetry #verification
A Complete Method for Symmetry Reduction in Safety Verification (DHC, JJ), pp. 616–633.
CAVCAV-2012-CimattiCLNRRST #industrial #validation #verification
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System (AC, RC, AL, IN, TR, MR, AS, AT), pp. 378–393.
CAVCAV-2012-JaffarMNS #execution #named #symbolic computation #verification
TRACER: A Symbolic Execution Tool for Verification (JJ, VM, JAN, AES), pp. 758–766.
CAVCAV-2012-Moskal #bound #c #infinity #verification
From C to Infinity and Back: Unbounded Auto-active Verification with VCC (MM), p. 6.
CAVCAV-2012-Myers #search-based #verification
Formal Verification of Genetic Circuits (CJM), p. 5.
ICSTICST-2012-AmraniLSCDVTC #approach #model transformation #verification
A Tridimensional Approach for Studying the Formal Verification of Model Transformations (MA, LL, GMKS, BC, JD, HV, YLT, JRC), pp. 921–928.
ICSTICST-2012-LiuNT #bound #case study #smt #using #verification
Bounded Program Verification Using an SMT Solver: A Case Study (TL, MN, MT), pp. 101–110.
ICSTICST-2012-TranP #framework #graph transformation #towards #verification
Towards a Rule-Level Verification Framework for Property-Preserving Graph Transformations (HNT, CP), pp. 946–953.
IJCARIJCAR-2012-BoerBR #automation #pointer #recursion #source code #verification
Automated Verification of Recursive Programs with Pointers (FSdB, MMB, JR), pp. 149–163.
IJCARIJCAR-2012-JacquelBDD #automation #deduction #modulo theories #proving #theorem proving #using #verification
Tableaux Modulo Theories Using Superdeduction — An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover (MJ, KB, DD, CD), pp. 332–338.
LICSLICS-2012-AgrawalAGT #approximate #markov #verification
Approximate Verification of the Symbolic Dynamics of Markov Chains (MA, SA, BG, PST), pp. 55–64.
LICSLICS-2012-EsparzaGM #bound #verification
A Perfect Model for Bounded Verification (JE, PG, RM), pp. 285–294.
RTARTA-2012-Lisitsa #automaton #finite #modelling #safety #verification
Finite Models vs Tree Automata in Safety Verification (AL), pp. 225–239.
ICSTSAT-2012-MarinMB #design #incremental #preprocessor #verification
Incremental QBF Preprocessing for Partial Design Verification — (Poster Presentation) (PM, CM, BB), pp. 473–474.
SMTSMT-2012-BjornerMR #modulo theories #satisfiability #verification
Program Verification as Satisfiability Modulo Theories (NB, KLM, AR), pp. 3–11.
SMTSMT-2012-GoelKLT #smt #verification
SMT-Based System Verification with DVF (AG, SK, RL, MRT), pp. 32–43.
VMCAIVMCAI-2012-AlbarghouthiGC #algorithm #interprocedural #named #verification
Whale: An Interpolation-Based Algorithm for Inter-procedural Verification (AA, AG, MC), pp. 39–55.
VMCAIVMCAI-2012-BasuBO #communication #verification
Synchronizability for Verification of Asynchronously Communicating Systems (SB, TB, MO), pp. 56–71.
VMCAIVMCAI-2012-BozzelliP #abstraction #constraints #verification
Verification of Gap-Order Constraint Abstractions of Counter Systems (LB, SP), pp. 88–103.
VMCAIVMCAI-2012-ChakiGS #concurrent #multi #source code #thread #verification
Regression Verification for Multi-threaded Programs (SC, AG, OS), pp. 119–135.
VMCAIVMCAI-2012-Jhala #verification
Software Verification with Liquid Types (RJ), p. 23.
VMCAIVMCAI-2012-NamjoshiT #composition #symmetry #verification
Local Symmetry and Compositional Verification (KSN, RJT), pp. 348–362.
ECSAECSA-2011-JohnsenPL #architecture #specification #verification
An Architecture-Based Verification Technique for AADL Specifications (AJ, PP, KL), pp. 105–113.
ASEASE-2011-ApelSWRB #detection #feature model #interactive #using #verification
Detection of feature interactions using feature-aware verification (SA, HS, PW, AvR, DB), pp. 372–375.
ASEASE-2011-IvancicBGSMTIM #bound #framework #named #scalability #verification
DC2: A framework for scalable, scope-bounded software verification (FI, GB, AG, SS, NM, HT, TI, YM), pp. 133–142.
CASECASE-2011-BallariniDDHP #composition #flexibility #modelling #petri net #verification
Petri nets compositional modeling and verification of Flexible Manufacturing Systems (PB, HD, MD, SH, NP), pp. 588–593.
CASECASE-2011-ThramboulidisSF #automation #industrial #process #safety #towards #verification
Towards an automated verification process for industrial safety applications (KT, DS, GF), pp. 482–487.
DACDAC-2011-AdirNSZMS #validation #verification
Leveraging pre-silicon verification resources for the post-silicon validation of the IBM POWER7 processor (AA, AN, GS, AZ, CM, JS), pp. 569–574.
DACDAC-2011-GhaniN #branch #grid #power management #using #verification
Power grid verification using node and branch dominance (NHAG, FNN), pp. 682–687.
DACDAC-2011-HolcombBS #performance #verification
Abstraction-based performance verification of NoCs (DEH, BAB, SAS), pp. 492–497.
DACDAC-2011-KadryMGAK #approach #challenge #design #effectiveness #verification
Facing the challenge of new design features: an effective verification approach (WK, RM, AG, EA, CAK), pp. 842–847.
DACDAC-2011-MoffittSV #clustering #functional #robust #verification
Robust partitioning for hardware-accelerated functional verification (MDM, MAS, PGV), pp. 854–859.
DACDAC-2011-NguyenWSK #abstraction #hardware
Formal hardware/software co-verification by interval property checking with abstraction (MDN, MW, DS, WK), pp. 510–515.
DACDAC-2011-RameshG #design #modelling #verification
Rigorous model-based design & verification flow for in-vehicle software (SR, AAG), pp. 13–16.
DATEDATE-2011-AdirCLNSZMS #validation #verification
A unified methodology for pre-silicon verification and post-silicon validation (AA, SC, SL, AN, GS, AZ, CM, JS), pp. 1590–1595.
DATEDATE-2011-BehrendLHRKR #embedded #hybrid #scalability #verification
Scalable hybrid verification for embedded software (JB, DL, PH, JR, TK, WR), pp. 179–184.
DATEDATE-2011-CroneBCDER #state of the art #verification
State of the art verification methodologies in 2015 (AC, OB, CC, BD, VE, MR), p. 1339.
DATEDATE-2011-GoyalN #grid #performance #power management #using #verification
Efficient RC power grid verification using node elimination (AG, FNN), pp. 257–260.
DATEDATE-2011-GuoCSCWH #debugging #design #empirical #predict #verification
Empirical design bugs prediction for verification (QG, TC, HS, YC, YW, WH), pp. 161–166.
DATEDATE-2011-JhaLMR #simulation #statistics #trade-off #verification
When to stop verification?: Statistical trade-off between expected loss and simulation cost (SKJ, CJL, SM, SR), pp. 1309–1314.
DATEDATE-2011-KapoorHT #case study #experience #power management #verification
Power management verification experiences in Wireless SoCs (BK, AH, PT), pp. 507–508.
DATEDATE-2011-KapoorJ #design #embedded #power management #tutorial #verification
Embedded tutorial: Addressing critical power management verification issues in low power designs (BK, KMJ), p. 124.
DATEDATE-2011-MatsudaI #debugging #verification
Developing an integrated verification and debug methodology (AM, TI), pp. 503–504.
DATEDATE-2011-PangrleBCDJ #design #power management #verification
Beyond UPF & CPF: Low-power design and verification (BMP, JB, CC, OD, KMJ), p. 252.
DATEDATE-2011-PavlenkoWSKDSG #algebra #named #problem #reasoning #smt #verification
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.
ICDARICDAR-2011-BeusekomS #automation #documentation #metric #verification
Distortion Measurement for Automatic Document Verification (JvB, FS), pp. 289–293.
ICDARICDAR-2011-LiwickiMHCBSBF #contest #online #verification
Signature Verification Competition for Online and Offline Skilled Forgeries (SigComp2011) (ML, MIM, CEvdH, XC, CB, RS, MB, BF), pp. 1480–1484.
ICDARICDAR-2011-NguyenB #2d #feature model #verification
An Application of the 2D Gaussian Filter for Enhancing Feature Extraction in Off-line Signature Verification (VN, MB), pp. 339–343.
ICDARICDAR-2011-NobileHSLS #verification
Digit/Symbol Pruning and Verification for Arabic Handwritten Digit/Symbol Spotting (NN, CLH, MWS, LL, CYS), pp. 648–652.
ICDARICDAR-2011-PanZSN11a #adaptation #detection #segmentation #verification
Improving Scene Text Detection by Scale-Adaptive Segmentation and Weighted CRF Verification (YFP, YZ, JS, SN), pp. 759–763.
ICDARICDAR-2011-ParodiGB #approach #feature model #invariant #verification
A Circular Grid-Based Rotation Invariant Feature Extraction Approach for Off-line Signature Verification (MP, JCG, AB), pp. 1289–1293.
ICDARICDAR-2011-WangWZ #graph #online #using #verification
On-line Signature Verification Using Segment-to-Segment Graph Matching (KW, YW, ZZ), pp. 804–808.
CSEETCSEET-2011-LiB #education #process #re-engineering #research #validation #verification
Making winners for both education and research: Verification and validation process improvement practice in a software engineering course (QL, BWB), pp. 304–313.
CSEETCSEET-2011-TuTOBHKY #learning
Turning real-world systems into verification-driven learning cases (ST, ST, SO, BB, BH, AK, ZY), pp. 129–138.
ITiCSEITiCSE-2011-VirsedaM #debugging #education #semantics #source code #verification
An innovative teaching tool based on semantic tableaux for verification and debugging of programs (RdVV, FPM), p. 352.
FoSSaCSFoSSaCS-2011-DelzannoSZ #ad hoc #clique #network #on the #power of #verification
On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks (GD, AS, GZ), pp. 441–455.
TACASTACAS-2011-ForejtKNPQ #multi #probability #verification
Quantitative Multi-objective Verification for Probabilistic Systems (VF, MZK, GN, DP, HQ), pp. 112–127.
TACASTACAS-2011-RavnSV #modelling #process #protocol #verification #web #web service
Modelling and Verification of Web Services Business Activity Protocol (APR, JS, SV), pp. 357–371.
PLDIPLDI-2011-Chlipala #logic #low level #source code #verification
Mostly-automated verification of low-level programs in computational separation logic (AC), pp. 234–245.
PLDIPLDI-2011-KimR #commutative #data type #linked data #open data #semantics #verification
Verification of semantic commutativity conditions and inverse operations on linked data structures (DK, MCR), pp. 528–541.
SASSAS-2011-DonaldsonHKR #using #verification
Software Verification Using k-Induction (AFD, LH, DK, PR), pp. 351–368.
SASSAS-2011-SchrammelJ #data flow #source code #verification
Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs (PS, BJ), pp. 233–248.
STOCSTOC-2011-SarmaHKKNPPW #approximate #distributed #verification
Distributed verification and hardness of distributed approximation (ADS, SH, LK, AK, DN, GP, DP, RW), pp. 363–372.
CIAACIAA-J-2010-YuBI11 #automaton #multi #relational #string #using #verification
Relational String Verification Using Multi-Track Automata (FY, TB, OHI), pp. 1909–1924.
FMFM-2011-BartheCK #relational #source code #using #verification
Relational Verification Using Product Programs (GB, JMC, CK), pp. 200–214.
FMFM-2011-BonakdarpourNF #runtime #verification
Sampling-Based Runtime Verification (BB, SN, SF), pp. 88–102.
FMFM-2011-DietschWP #verification
System Verification through Program Verification (DD, BW, AP), pp. 27–41.
FMFM-2011-GherghinaDQC #source code #specification #verification
Structured Specifications for Better Verification of Heap-Manipulating Programs (CG, CD, SQ, WNC), pp. 386–401.
FMFM-2011-HaxthausenKB #automation #development #modelling #verification
Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems (AEH, AAK, MLB), pp. 118–132.
FMFM-2011-JacobsSP #verification
Verification of Unloadable Modules (BJ, JS, FP), pp. 402–416.
FMFM-2011-MeryMT #algorithm #verification
Refinement-Based Verification of Local Synchronization Algorithms (DM, MM, MT), pp. 338–352.
FMFM-2011-MullerR #using #verification
Using Debuggers to Understand Failed Verification Attempts (PM, JNR), pp. 73–87.
FMFM-2011-QinLCH #automation #specification #verification
Automatically Refining Partial Specifications for Program Verification (SQ, CL, WNC, GH), pp. 369–385.
SEFMSEFM-2011-BlechB #coq #semantics #verification
Verification of PLC Properties Based on Formal Semantics in Coq (JOB, SOB), pp. 58–73.
SEFMSEFM-2011-BubelHG #formal method #java #specification #string #verification
A Formalisation of Java Strings for Program Specification and Verification (RB, RH, UG), pp. 90–105.
SEFMSEFM-2011-CastroKAA #branch #fault tolerance #logic #named #verification
dCTL: A Branching Time Temporal Logic for Fault-Tolerant System Verification (PFC, CK, AA, NA), pp. 106–121.
SEFMSEFM-2011-ErnstSR #analysis #empirical #interactive #proving #theorem proving #verification
Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving (GE, GS, WR), pp. 188–203.
SEFMSEFM-2011-FalconeJNBB #component #runtime #verification
Runtime Verification of Component-Based Systems (YF, MJ, THN, MB, SB), pp. 204–220.
SEFMSEFM-2011-GouesLM #debugging #verification
The Boogie Verification Debugger (Tool Paper) (CLG, KRML, MM), pp. 407–414.
SEFMSEFM-2011-ParrinoGGF #analysis #bound #data flow #satisfiability #verification
A Dataflow Analysis to Improve SAT-Based Bounded Program Verification (BCP, JPG, DG, MFF), pp. 138–154.
SEFMSEFM-2011-SoleimanifardGH #composition #named #safety #verification
ProMoVer: Modular Verification of Temporal Safety Properties (SS, DG, MH), pp. 366–381.
SEFMSEFM-2011-TschannenFNM #object-oriented #source code #verification
Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques (JT, CAF, MN, BM), pp. 382–398.
SFMSFM-2011-BaierKK #component #modelling #verification
Modeling and Verification of Components and Connectors (CB, JK, SK), pp. 114–147.
SFMSFM-2011-ForejtKNP #automation #probability #verification
Automated Verification Techniques for Probabilistic Systems (VF, MZK, GN, DP), pp. 53–113.
ICFPICFP-2011-Chargueraud #imperative #source code #verification
Characteristic formulae for the verification of imperative programs (AC), pp. 418–430.
ICFPICFP-2011-GotsmanY #composition #kernel #verification
Modular verification of preemptive OS kernels (AG, HY), pp. 404–417.
IFLIFL-2011-Page #testing #verification
Property-Based Testing and Verification: A Catalog of Classroom Examples (RP), pp. 134–147.
HCIHCI-ITE-2011-LinD #modelling #verification
Verification of Two Models of Ballistic Movements (JFL, CGD), pp. 275–284.
HCIHCI-MIIE-2011-RiahiRM #generative #human-computer #mobile #specification #verification #xml
XML in Formal Specification, Verification and Generation of Mobile HCI (IR, MR, FM), pp. 92–100.
AdaEuropeAdaEurope-2011-CarnevaliLPV #approach #design #formal method #scheduling #verification
A Formal Approach to Design and Verification of Two-Level Hierarchical Scheduling Systems (LC, GL, AP, EV), pp. 118–131.
SEKESEKE-2011-DengLSW #api #constraints #runtime #specification #verification
Specification and Runtime Verification of API Constraints on Interacting Objects (FD, HL, JS, QW), pp. 101–106.
ECMFAECMFA-2011-CariouBFB #contract #execution #verification
Contracts for Model Execution Verification (EC, CB, AF, FB), pp. 3–18.
ECMFAECMFA-2011-ElaasarBL #qvt #verification
Domain-Specific Model Verification with QVT (ME, LCB, YL), pp. 282–298.
ECMFAECMFA-2011-JurjensMOS #evolution #incremental #modelling #security #verification
Incremental Security Verification for Evolving UMLsec models (JJ, LM, MO, HS), pp. 52–68.
MODELSMoDELS-2011-StenzelMR #code generation #qvt #verification
Formal Verification of QVT Transformations for Code Generation (KS, NM, WR), pp. 533–547.
MODELSMoDELS-2011-StenzelMR #code generation #qvt #verification
Formal Verification of QVT Transformations for Code Generation (KS, NM, WR), pp. 533–547.
OnwardOnward-2011-Bierhoff #automation #lightweight #reasoning #verification
Automated program verification made SYMPLAR: symbolic permissions for lightweight automated reasoning (KB), pp. 19–32.
OOPSLAOOPSLA-2011-DavidC #precise #specification #verification
Immutable specifications for more concise and precise verification (CD, WNC), pp. 359–374.
OOPSLAOOPSLA-2011-MadhavanK #analysis #approximate #null #verification
Null dereference verification via over-approximated weakest pre-conditions analysis (RM, RK), pp. 1033–1052.
PPDPPPDP-2011-InabaHHKN #higher-order #logic #monad #using #verification
Graph-transformation verification using monadic second-order logic (KI, SH, ZH, HK, KN), pp. 17–28.
PPDPPPDP-2011-Rybalchenko #automation #synthesis #tool support #towards #verification
Towards automatic synthesis of software verification tools (AR), pp. 3–4.
POPLPOPL-2011-AlurC #algorithm #source code #streaming #transducer #verification
Streaming transducers for algorithmic verification of single-pass list-processing programs (RA, PC), pp. 599–610.
POPLPOPL-2011-EsparzaG #complexity #parallel #source code #thread #verification
Complexity of pattern-based verification for multithreaded programs (JE, PG), pp. 499–510.
POPLPOPL-2011-GordonHHJS #concurrent #verification
Robin Milner 1934--2010: verification, languages, and concurrency (ADG, RH, JH, AJ, PS), pp. 473–474.
POPLPOPL-2011-RamananandroRL #c++ #inheritance #layout #multi #verification
Formal verification of object layout for c++ multiple inheritance (TR, GDR, XL), pp. 67–80.
SACSAC-2011-ChuHLCHC #approach #development #manycore #verification
A pattern-based verification approach for a multi-core system development (PHC, NLH, CCL, MJC, PAH, WCC), pp. 49–53.
SACSAC-2011-DumasDBB #partial order #verification
Application of partial-order methods for the verification of closed-loop SDL systems (XD, PD, FB, EB), pp. 1666–1673.
SACSAC-2011-Muramatsu #algorithm #online #random #verification
Random forgery attacks against DTW-based online signature verification algorithm (DM), pp. 27–28.
SACSAC-2011-RayNDF #interactive #privacy #verification
Verification of data pattern for interactive privacy preservation model (SR, MFN, SD, BCMF), pp. 1716–1723.
SACSAC-2011-ZhuWHAHY #outsourcing #verification
Dynamic audit services for integrity verification of outsourced storages in clouds (YZ, HW, ZH, GJA, HH, SSY), pp. 1550–1557.
ESEC-FSEESEC-FSE-2011-Filieri #runtime #verification
QoS verification and model tuning @ runtime (AF), pp. 408–411.
ESEC-FSEESEC-FSE-2011-MontrieuxWY #data access #specification #tool support #uml #verification
Tool support for UML-based specification and verification of role-based access control properties (LM, MW, YY), pp. 456–459.
ESEC-FSEESEC-FSE-2011-NaudziunieneBDDGP #automation #ide #java #named #source code #verification
jStar-eclipse: an IDE for automated verification of Java programs (DN, MB, DD, MD, RG, MJP), pp. 428–431.
ICSEICSE-2011-GeTXT #execution #named #symbolic computation #verification
DyTa: dynamic symbolic execution guided with static verification results (XG, KT, TX, NT), pp. 992–994.
ICSEICSE-2011-RosuS #approach #logic #verification
Matching logic: a new program verification approach (GR, AS), pp. 868–871.
ASPLOSASPLOS-2011-RyzhykKMRVH #hardware #reliability #reuse #verification
Improved device driver reliability through hardware verification reuse (LR, JK, BM, AR, MV, GH), pp. 133–144.
PPoPPPPoPP-2011-SiegelZ #automation #parallel #source code #verification
Automatic formal verification of MPI-based parallel programs (SFS, TKZ), pp. 309–310.
CAVCAV-2011-AlkassarBMR #verification
Verification of Certifying Computations (EA, SB, KM, CR), pp. 67–82.
CAVCAV-2011-BeyerK #configuration management #named #verification
CPAchecker: A Tool for Configurable Software Verification (DB, MEK), pp. 184–190.
CAVCAV-2011-ChinGVLCQ #calculus #verification
A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification (WNC, CG, RV, QLL, FC, SQ), pp. 293–309.
CAVCAV-2011-CimattiMT #automaton #hybrid #performance #verification
Efficient Scenario Verification for Hybrid Automata (AC, SM, ST), pp. 317–332.
CAVCAV-2011-CookKV #program analysis #verification
Temporal Property Verification as a Program Analysis Task (BC, EK, MYV), pp. 333–348.
CAVCAV-2011-FrehseGDCRLRGDM #hybrid #named #scalability #verification
SpaceEx: Scalable Verification of Hybrid Systems (GF, CLG, AD, SC, RR, OL, RR, AG, TD, OM), pp. 379–395.
CAVCAV-2011-HabermehlHRSV #automaton #verification
Forest Automata for Verification of Heap Manipulation (PH, LH, AR, JS, TV), pp. 424–440.
CAVCAV-2011-Jhala #using #verification
Using Types for Software Verification (RJ), p. 20.
CAVCAV-2011-KleinN #automation #behaviour #formal method #rest #verification
Formalization and Automated Verification of RESTful Behavior (UK, KSN), pp. 541–556.
CAVCAV-2011-KroeningW #verification
Interpolation-Based Software Verification with Wolverine (DK, GW), pp. 573–578.
CAVCAV-2011-KwiatkowskaNP #probability #realtime #verification
PRISM 4.0: Verification of Probabilistic Real-Time Systems (MZK, GN, DP), pp. 585–591.
CAVCAV-2011-MullerP #hardware #interface #verification
Complete Formal Hardware Verification of Interfaces for a FlexRay-Like Bus (CAM, WJP), pp. 633–648.
CAVCAV-2011-PeterEM #automaton #named #synthesis #verification
Synthia: Verification and Synthesis for Timed Automata (HJP, RE, RM), pp. 649–655.
CAVCAV-2011-Platzer #composition #hybrid #logic #tutorial #verification
Logic and Compositional Verification of Hybrid Systems — (Invited Tutorial) (AP), pp. 28–43.
CAVCAV-2011-RamosE #equivalence #verification
Practical, Low-Effort Equivalence Verification of Real Code (DAR, DRE), pp. 669–685.
CAVCAV-2011-SinghalA #simulation #using #verification
Using Coverage to Deploy Formal Verification in a Simulation World (VS, PA), pp. 44–49.
ICSTICST-2011-Bhattacharya #hybrid #verification
SoftwareHardware Hybrid Systems Verification (NB), pp. 435–438.
ICSTICST-2011-RubanovS #kernel #linux #runtime #verification
Runtime Verification of Linux Kernel Modules Based on Call Interception (VVR, EAS), pp. 180–189.
ISSTAISSTA-2011-NijjarB #bound #modelling #ruby #verification
Bounded verification of Ruby on Rails data models (JN, TB), pp. 67–77.
TAPTAP-2011-SoekenWD #data type #encoding #modelling #ocl #satisfiability #uml #verification
Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models (MS, RW, RD), pp. 152–170.
VMCAIVMCAI-2011-Logozzo #abstract interpretation #verification
Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation — (Invited Talk) (FL), pp. 19–22.
ASEASE-2010-BorgesGL #adaptation #self #verification
Integrating model verification and self-adaptation (RVB, ASdG, LCL), pp. 317–320.
ASEASE-2010-ShaikhCWM #modelling #ocl #slicing #uml
Verification-driven slicing of UML/OCL models (AS, RC, UKW, NM), pp. 185–194.
DACDAC-2010-HazraMDPBG #architecture #modelling #verification
Leveraging UPF-extracted assertions for modeling and formal verification of architectural power intent (AH, SM, PD, AP, DB, KG), pp. 773–776.
DACDAC-2010-KundertC #functional #modelling #verification
Model-based functional verification (KSK, HC), pp. 421–424.
DACDAC-2010-LiFS #mining #scalability #specification #verification
Scalable specification mining for verification and diagnosis (WL, AF, SAS), pp. 755–760.
DACDAC-2010-NahirZGHACBFBK #validation #verification
Bridging pre-silicon verification and post-silicon validation (AN, AZ, RG, AJH, MA, AC, BB, HF, VB, SK), pp. 94–95.
DACDAC-2010-ThomptoH #fault tolerance #verification
Verification for fault tolerance of the IBM system z microprocessor (BWT, BH), pp. 525–530.
DACDAC-2010-XiongW #algorithm #constraints #grid #linear #performance #power management #verification
An efficient dual algorithm for vectorless power grid verification under linear current constraints (XX, JW), pp. 837–842.
DATEDATE-2010-BraunBLR #interface #specification #verification
Simulation-based verification of the MOST NetInterface specification revision 3.0 (AB, OB, DL, WR), pp. 538–543.
DATEDATE-2010-FerroP #modelling #semantics #transaction #verification
Formal semantics for PSL modeling layer and application to the verification of transactional models (LF, LP), pp. 1207–1212.
DATEDATE-2010-LammermannRKRVJH #design #towards #verification
Towards assertion-based verification of heterogeneous system designs (SL, JR, TK, WR, AV, AJ, LH), pp. 1171–1176.
DATEDATE-2010-NarayananAZTP #process #verification
Formal verification of analog circuits in the presence of noise and process variation (RN, BA, MHZ, ST, LCP), pp. 1309–1312.
DATEDATE-2010-OliveiraZ0 #verification
Assertion-based verification of RTOS properties (MFdSO, HZ, WM), pp. 630–633.
DATEDATE-2010-ZhangLL #approach #markov #modelling #simulation #using #verification
An abstraction-guided simulation approach using Markov models for microprocessor verification (TZ, TL, XL), pp. 484–489.
ITiCSEITiCSE-2010-TuOKKT #learning
Developing verification-driven learning cases (ST, SJO, RK, AK, ST), pp. 58–62.
ESOPESOP-2010-AmtoftHR #array #automation #certification #contract #data flow #precise #reasoning #source code #verification
Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays (TA, JH, ER), pp. 43–63.
ESOPESOP-2010-BlazyRA #graph #verification
Formal Verification of Coalescing Graph-Coloring Register Allocation (SB, BR, AWA), pp. 145–164.
FASEFASE-2010-EhrigERBP #analysis #formal method #self #verification
Formal Analysis and Verification of Self-Healing Systems (HE, CE, OR, AB, PP), pp. 139–153.
FASEFASE-2010-LiXBLM #approach #hardware
An Automata-Theoretic Approach to Hardware/Software Co-verification (JL, FX, TB, VL, CM), pp. 248–262.
TACASTACAS-2010-KatzP #automation #verification
Code Mutation in Verification and Automatic Code Correction (GK, DP), pp. 435–450.
TACASTACAS-2010-KwiatkowskaNPQ #probability #verification
Assume-Guarantee Verification for Probabilistic Systems (MZK, GN, DP, HQ), pp. 23–37.
TACASTACAS-2010-LeinoR #design #encoding #logic #polymorphism #verification
A Polymorphic Intermediate Verification Language: Design and Logical Encoding (KRML, PR), pp. 312–327.
ICSMEICSM-2010-PonsiniCFMR #automation #invariant #verification
Automatic verification of loop invariants (OP, HC, CF, CM, MR), pp. 1–5.
PLDIPLDI-2010-ChenCS #compilation #security #verification
Type-preserving compilation of end-to-end verification of security enforcement (JC, RC, NS), pp. 412–423.
PLDIPLDI-2010-EmmiMM #transaction #verification
Parameterized verification of transactional memories (ME, RM, RM), pp. 134–145.
PLDIPLDI-2010-YangH #automation #operating system #type safety #verification
Safe to the last instruction: automated verification of a type-safe operating system (JY, CH), pp. 99–110.
SASSAS-2010-Fahndrich #contract #verification
Static Verification for Code Contracts (MF), pp. 2–5.
SASSAS-2010-VechevYRS #automation #parallel #source code #verification
Automatic Verification of Determinism for Structured Parallel Programs (MTV, EY, RR, VS), pp. 455–471.
CIAACIAA-2010-YuBI #automaton #multi #relational #string #using #verification
Relational String Verification Using Multi-track Automata (FY, TB, OHI), pp. 290–299.
ICALPICALP-v1-2010-ApplebaumIK #performance #verification
From Secrecy to Soundness: Efficient Verification via Secure Computation (BA, YI, EK), pp. 152–163.
ICALPICALP-v2-2010-Goubault-Larrecq #verification
Noetherian Spaces in Verification (JGL), pp. 2–21.
ICALPICALP-v2-2010-OuaknineW #bound #formal method #towards #verification
Towards a Theory of Time-Bounded Verification (JO, JW), pp. 22–37.
IFMIFM-2010-AutexierL #c #impact analysis #source code #verification
Adding Change Impact Analysis to the Formal Verification of C Programs (SA, CL), pp. 59–73.
IFMIFM-2010-Faber #architecture #composition #realtime #reasoning #verification
Verification Architectures: Compositional Reasoning for Real-Time Systems (JF), pp. 136–151.
IFMIFM-2010-FaberIJS #automation #parametricity #specification #verification
Automatic Verification of Parametric Specifications with Complex Topologies (JF, CI, SJ, VSS), pp. 152–167.
IFMIFM-2010-LanoR #model transformation #specification #uml #using #verification
Specification and Verification of Model Transformations Using UML-RSDS (KL, SKR), pp. 199–214.
SEFMSEFM-2010-BersaniCFPR #constraints #integer #ltl #runtime #smt #specification #verification
SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability (MMB, LC, AF, MP, MR), pp. 244–254.
SEFMSEFM-2010-GallardoS #calculus #verification #μ-calculus
Verification of Dynamic Data Tree with μ-calculus Extended with Separation (MdMG, DS), pp. 211–221.
SEFMSEFM-2010-Ghezzi #adaptation #verification
Adaptive Software Needs Continuous Verification (CG), pp. 3–4.
SEFMSEFM-2010-Giannakopoulou #quote #verification
“Fly Me to the Moon”: Verification of Aerospace Systems (DG), pp. 5–11.
SEFMSEFM-2010-GothelG #automation #invariant #network #realtime #towards #using #verification
Towards the Semi-Automatic Verification of Parameterized Real-Time Systems Using Network Invariants (TG, SG), pp. 310–314.
ICFPICFP-2010-Chargueraud #verification
Program verification through characteristic formulae (AC), pp. 321–332.
GT-VMTGT-VMT-2010-Schatz #model transformation #verification
Verification of Model Transformations (BS).
ICGTICGT-2010-Blume #graph #verification
Recognizable Graph Languages for the Verification of Dynamic Systems (CB), pp. 384–387.
ICGTICGT-2010-KonigE #graph transformation #specification #verification
Verification of Graph Transformation Systems with Context-Free Specifications (BK, JE), pp. 107–122.
ICGTICGT-2010-Zambon #abstraction #graph transformation #using #verification
Using Graph Transformations and Graph Abstractions for Software Verification (EZ), pp. 416–418.
AdaEuropeAdaEurope-2010-BritoP #case study #comparative #verification
Program Verification in SPARK and ACSL: A Comparative Case Study (EB, JSP), pp. 97–110.
CAiSECAiSE-2010-LyRD #design #graph #information management #verification
Design and Verification of Instantiable Compliance Rule Graphs in Process-Aware Information Systems (LTL, SRM, PD), pp. 9–23.
ICEISICEIS-ISAS-2010-MoralesTP #composition #process #verification
Compositional Verification of Business Processes Modelled with BPMN (LEMM, MICT, MAP), pp. 113–122.
ICEISICEIS-ISAS-2010-RajiD #framework #modelling
User Context Models — A Framework to Ease Software Formal Verifications (AR, PD), pp. 380–383.
ICEISICEIS-J-2010-MoralesTP10a #composition #formal method #process #verification
A Formalization Proposal of Timed BPMN for Compositional Verification of Business Processes (LEMM, MICT, MAP), pp. 388–403.
ICPRICPR-2010-BatistaGS #difference #representation #verification
Applying Dissimilarity Representation to Off-Line Signature Verification (LB, EG, RS), pp. 1293–1297.
ICPRICPR-2010-BourlaiKRCH #verification
Cross-Spectral Face Verification in the Short Wave Infrared (SWIR) Band (TB, NDK, AR, BC, LH), pp. 1343–1347.
ICPRICPR-2010-BrewC #verification
Vector Quantization Mappings for Speaker Verification (AB, PC), pp. 560–564.
ICPRICPR-2010-BuyssensR #learning #verification
Learning Sparse Face Features: Application to Face Verification (PB, MR), pp. 670–673.
ICPRICPR-2010-GaoEFS #multi #verification
Multi-resolution Local Appearance-Based Face Verification (HG, HKE, MF, RS), pp. 1501–1504.
ICPRICPR-2010-GuichardTC #novel #recognition #verification #word
A Novel Verification System for Handwritten Words Recognition (LG, AHT, BC), pp. 2869–2872.
ICPRICPR-2010-HeLS #automation #recognition #verification
Automatic Discrimination between Confusing Classes with Writing Styles Verification in Arabic Handwritten Numeral Recognition (CLH, LL, CYS), pp. 2045–2048.
ICPRICPR-2010-HendrikseVS #verification
Verification Under Increasing Dimensionality (AH, RNJV, LJS), pp. 589–592.
ICPRICPR-2010-IbrahimKKG #analysis #online #using #verification
On-Line Signature Verification Using 1-D Velocity-Based Directional Analysis (MTI, MJK, MAK, LG), pp. 3830–3833.
ICPRICPR-2010-Lei #distance #using #verification
Combining the Likelihood and the Kullback-Leibler Distance in Estimating the Universal Background Model for Speaker Verification Using SVM (ZL), pp. 4553–4556.
ICPRICPR-2010-LiD #classification #multi #verification
Multi-classifier Q-stack Aging Model for Adult Face Verification (WL, AD), pp. 1310–1313.
ICPRICPR-2010-LvBYD #using #verification #visual notation
Off-Line Signature Verification Using Graphical Model (HL, XB, WY, JD), pp. 3784–3788.
ICPRICPR-2010-MemonLM #modelling #verification
Information Theoretic Expectation Maximization Based Gaussian Mixture Modeling for Speaker Verification (SM, ML, NCM), pp. 4536–4540.
ICPRICPR-2010-PuS #learning #probability #verification
Probabilistic Measure for Signature Verification Based on Bayesian Learning (DP, SNS), pp. 1188–1191.
ICPRICPR-2010-VillegasP #verification #video
Fusion of Qualities for Frame Selection in Video Face Verification (MV, RP), pp. 1302–1305.
ICPRICPR-2010-WilliamsTSB #analysis #multi #verification
Body Motion Analysis for Multi-modal Identity Verification (GW, GWT, KS, CB), pp. 2198–2201.
ICPRICPR-2010-ZafrullaBYPSH #education #game studies #verification
American Sign Language Phrase Verification in an Educational Game for Deaf Children (ZZ, HB, PY, PP, TS, HH), pp. 3846–3849.
KEODKEOD-2010-AnjumHY #ontology #verification
Cross Domain Knowledge Verification — Verifying Knowledge in Foundation Ontology based Domain Ontologies (NAA, JAH, BY), pp. 339–342.
KEODKEOD-2010-KezadriP #ontology #towards #validation #verification
First Steps Toward a Verification and Validation Ontology (MK, MP), pp. 440–444.
KMISKMIS-2010-LodemannL #framework #ontology #verification
Ontology-based Railway Infrastructure Verification — Planning Benefits (ML, NL), pp. 176–181.
SEKESEKE-2010-BernhartAMG #automation #case study #experience #framework #integration #testing #verification
Automated Integration Testing and Verification of a Secured SOA Infrastructure — an Experience Report in eHealth (MB, TA, AM, TG), pp. 198–202.
SEKESEKE-2010-BinGHMMPRST #hardware #ontology #tool support #verification
Ontology-Based Tools in the Service of Hardware Verification (EB, AG, KH, EM, RM, OP, MR, GS, ET), pp. 303–308.
SEKESEKE-2010-GoelXS #multi #network #online #verification
A Multi-State Bayesian Network for Shill Verification in Online Auctions (AG, HX, SMS), pp. 279–285.
SEKESEKE-2010-ParkHK #diagrams #sequence chart #uml #verification
Formal Verification of UML 2.0 Sequence Diagram (SP, TH, GK), pp. 411–416.
SIGIRSIGIR-2010-Roussinov #aspect-oriented #verification
Aspect presence verification conditional on other aspects (DR), pp. 865–866.
LOPSTRLOPSTR-2010-GiorginoSMP #algorithm #graph #verification
Verification of the Schorr-Waite Algorithm — From Trees to Graphs (MG, MS, RM, MP), pp. 67–83.
PPDPPPDP-2010-JacquemardR #verification #xml
Rewrite-based verification of XML updates (FJ, MR), pp. 119–130.
QAPLQAPL-2010-BarsottiW #abstraction #automation #probability #random #verification
Automatic Probabilistic Program Verification through Random Variable Abstraction (DB, NW), pp. 34–47.
POPLPOPL-2010-AtigBBM #memory management #modelling #on the #problem #verification
On the verification problem for weak memory models (MFA, AB, SB, MM), pp. 7–18.
POPLPOPL-2010-AttiyaRR #verification
Sequential verification of serializability (HA, GR, NR), pp. 31–42.
POPLPOPL-2010-BhargavanFG #composition #protocol #security #type system #verification
Modular verification of security protocol code by typing (KB, CF, ADG), pp. 445–456.
POPLPOPL-2010-KobayashiTU #higher-order #multi #recursion #transducer #verification
Higher-order multi-parameter tree transducers and recursion schemes for program verification (NK, NT, HU), pp. 495–508.
POPLPOPL-2010-NanevskiVB #source code #verification
Structuring the verification of heap-manipulating programs (AN, VV, JB), pp. 261–274.
POPLPOPL-2010-SrivastavaGF #synthesis #verification
From program verification to program synthesis (SS, SG, JSF), pp. 313–326.
REFSQREFSQ-2010-SabaliauskaiteLEURRGF #challenge #industrial #requirements #scalability #verification
Challenges in Aligning Requirements Engineering and Verification in a Large-Scale Industrial Context (GS, AL, EE, MU, BR, PR, TG, RF), pp. 128–142.
SACSAC-2010-CiraciBA #constraints #graph #verification
Graph-based verification of static program constraints (SC, PvdB, MA), pp. 2265–2272.
SACSAC-2010-GehlertBKMPP #adaptation #verification
Exploiting assumption-based verification for the adaptation of service-based applications (AG, AB, RK, AM, MP, KP), pp. 2430–2437.
SACSAC-2010-HurnausP #automation #composition #contract #programming #verification
Programming assistance based on contracts and modular verification in the automation domain (DH, HP), pp. 2544–2551.
SACSAC-2010-IqbalKFD #email #forensics #verification
e-mail authorship verification for forensic investigation (FI, LAK, BCMF, MD), pp. 1591–1598.
SACSAC-2010-KokashKV #composition #design #verification
Data-aware design and verification of service compositions with Reo and mCRL2 (NK, CK, EPdV), pp. 2406–2413.
SACSAC-2010-RoyM #verification #visual notation
Visual processing-inspired fern-audio features for noise-robust speaker verification (AR, SM), pp. 1491–1495.
SACSAC-2010-VogelsJP #generative #performance #proving #verification
A machine-checked soundness proof for an efficient verification condition generator (FV, BJ, FP), pp. 2517–2522.
FSEFSE-2010-LiG #gpu #kernel #scalability #smt #verification
Scalable SMT-based verification of GPU kernel functions (GL, GG), pp. 187–196.
ICSEICSE-2010-ClassenHSLR #model checking #performance #product line #verification
Model checking lots of systems: efficient verification of temporal properties in software product lines (AC, PH, PYS, AL, JFR), pp. 335–344.
ICSEICSE-2010-Elmas #abstraction #concurrent #named #proving #reduction #verification
QED: a proof system based on reduction and abstraction for the static verification of concurrent software (TE), pp. 507–508.
ICSEICSE-2010-YangL #approach #bound #verification
A cut-off approach for bounded verification of parameterized systems (QY, ML), pp. 345–354.
LDTALDTA-J-2007-CamachoMBV #automation #generative #tool support #using #verification
Automated generation of program translation and verification tools using annotated grammars (DOC, KM, MvdB, JJV), pp. 3–20.
LDTALDTA-2010-CruzHP #analysis #named #online #verification
GamaSlicer: an online laboratory for program verification and analysis (DCdC, PRH, JSP), p. 3.
CAVCAV-2010-BraytonM #named #verification
ABC: An Academic Industrial-Strength Verification Tool (RKB, AM), pp. 24–40.
CAVCAV-2010-CohenMST #concurrent #invariant #source code #verification
Local Verification of Global Invariants in Concurrent Programs (EC, MM, WS, ST), pp. 480–494.
CAVCAV-2010-Donze #hybrid #parametricity #synthesis #verification
Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems (AD), pp. 167–170.
CAVCAV-2010-KawaguchiRJ #named #safety #verification
Dsolve: Safety Verification via Liquid Types (MK, PMR, RJ), pp. 123–126.
CAVCAV-2010-LiXBL #analysis #automaton #hardware #performance #reachability
Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification (JL, FX, TB, VL), pp. 339–353.
CAVCAV-2010-McMillan #lazy evaluation #testing #verification
Lazy Annotation for Program Testing and Verification (KLM), pp. 104–118.
CAVCAV-2010-PnueliSZ #algorithm #framework #named #verification
Jtlv: A Framework for Developing Verification Algorithms (AP, YS, LDZ), pp. 171–174.
CAVCAV-2010-PulinaT #abstraction #approach #network #verification
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks (LP, AT), pp. 243–257.
CAVCAV-2010-Rybalchenko #constraints #theorem proving #theory and practice #verification
Constraint Solving for Program Verification: Theory and Practice by Example (AR), pp. 57–71.
CAVCAV-2010-ZhangSRHH #hybrid #probability #safety #verification
Safety Verification for Probabilistic Hybrid Systems (LZ, ZS, SR, HH, EMH), pp. 196–211.
CSLCSL-2010-Rybalchenko #constraints #theorem proving #theory and practice #verification
Constraint Solving for Program Verification: Theory and Practice by Example (AR), p. 51.
ICLPICLP-2010-Lopez-GarciaDB10 #debugging #framework #resource management #verification
A Framework for Verification and Debugging of Resource Usage Properties: Resource Usage Verification (PLG, LD, FB), pp. 104–113.
ICSTICST-2010-AsztalosLL #automation #model transformation #towards #verification
Towards Automated, Formal Verification of Model Transformations (MA, LL, TL), pp. 15–24.
ICSTICST-2010-FeldtTAR #challenge #industrial #process #validation #verification
Challenges with Software Verification and Validation Activities in the Space Industry (RF, RT, EA, BR), pp. 225–234.
ICSTICST-2010-Laurent #concept #formal method #process #testing #using #validation #verification
Using Formal Methods and Testability Concepts in the Avionics Systems Validation and Verification (V&V) Process (OL), pp. 1–10.
IJCARIJCAR-2010-AyadM #float #multi #source code #verification
Multi-Prover Verification of Floating-Point Programs (AA, CM), pp. 127–141.
IJCARIJCAR-2010-Sofronie-Stokkermans #parametricity #reasoning #verification
Hierarchical Reasoning for the Verification of Parametric Systems (VSS), pp. 171–187.
ISSTAISSTA-2010-GaleottiRPF #analysis #bound #invariant #performance #verification
Analysis of invariants for efficient bounded verification (JPG, NR, CLP, MFF), pp. 25–36.
LICSLICS-2010-Moore #proving #theorem proving #verification
Theorem Proving for Verification: The Early Days (JSM), p. 283.
TAPTAP-2010-AhnD #axiom #first-order #logic #testing #verification
Testing First-Order Logic Axioms in Program Verification (KYA, ED), pp. 22–37.
TAPTAP-2010-GladischTBY #generative #testing #using #verification
Generating Regression Unit Tests Using a Combination of Verification and Capture & Replay (CG, SST, BB, AY), pp. 61–76.
VMCAIVMCAI-2010-BuZL #automaton #hybrid #programming #reachability #using #verification
Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming (LB, JZ, XL), pp. 78–94.
VMCAIVMCAI-2010-ChadhaLPV #bound #complexity #realtime #verification
Complexity Bounds for the Verification of Real-Time Software (RC, AL, PP, MV), pp. 95–111.
WICSA-ECSAWICSA-ECSA-2009-BucchiaronePVR #modelling #self #using #verification
Self-Repairing systems modeling and verification using AGG (AB, PP, CV, OR), pp. 181–190.
ASEASE-2009-DenneyF #approach #documentation #traceability
A Verification-Driven Approach to Traceability and Documentation for Auto-Generated Mathematical Software (ED, BF), pp. 560–564.
ASEASE-2009-Jenson #component #constraints #dependence #validation #verification
Improving Component Dependency Resolution with Soft Constraints, Validation and Verification (GJ), pp. 716–720.
ASEASE-2009-RayMACSM #using #validation #verification
Validating Automotive Control Software Using Instrumentation-Based Verification (AR, IM, CA, RC, CPS, CM), pp. 15–25.
CASECASE-2009-AlenljungL #graph #using #verification
Formal verification of PLC controlled systems using Sensor Graphs (TA, BL), pp. 164–170.
CASECASE-2009-AllenGT #logic #nondeterminism #verification
Closed-loop determinism for non-deterministic environments: Verification for IEC 61499 logic controllers (LVA, KMG, DMT), pp. 1–6.
CASECASE-2009-VoronovA #model checking #process #using #verification
Verification of process operations using model checking (AV, ), pp. 415–420.
DACDAC-2009-AlimohammadFC #verification
FPGA-based accelerator for the verification of leading-edge wireless systems (AA, SFF, BFC), pp. 844–847.
DACDAC-2009-Chesters #development #lifecycle #verification
Role of the verification team throughout the ASIC development life cycle (EC), pp. 216–219.
DACDAC-2009-GhaniN #approximate #grid #performance #power management #using #verification
Fast vectorless power grid verification using an approximate inverse technique (NHAG, FNN), pp. 184–189.
DACDAC-2009-GluskaL #modelling #verification
Shortening the verification cycle with synthesizable abstract models (AG, LL), pp. 454–459.
DACDAC-2009-GodlinS #verification
Regression verification (BG, OS), pp. 466–471.
DACDAC-2009-MarcilioSAR #behaviour #novel #verification
A novel verification technique to uncover out-of-order DUV behaviors (GM, LCVdS, BA, SR), pp. 448–453.
DACDAC-2009-RanjanCS #debugging #verification
Beyond verification: leveraging formal for debugging (RKR, CC, SS), pp. 648–651.
DACDAC-2009-StapletonT #component #design #problem #reuse #verification
Verification problems in reusing internal design components (WS, PT), pp. 209–211.
DACDAC-2009-Thaker #question #verification
Holistic verification: myth or magic bullet? (PAT), pp. 204–208.
DACDAC-2009-Whipp #architecture #process #verification
Exploiting “architecture for verification” to streamline the verification process (DW), pp. 212–215.
DATEDATE-2009-AlimohammadFC #algorithm #architecture #development #flexibility #verification
A flexible layered architecture for accurate digital baseband algorithm development and verification (AA, SFF, BFC), pp. 45–50.
DATEDATE-2009-BarkeGGHHPSW #formal method #verification
Formal approaches to analog circuit verification (EB, DG, HG, LH, SH, RP, SS, YW), pp. 724–729.
DATEDATE-2009-BombieriFPHL #functional #verification
Functional qualification of TLM verification (NB, FF, GP, MH, FL), pp. 190–195.
DATEDATE-2009-CabodiCGMNQ #constraints #model checking #verification
Speeding up model checking by exploiting explicit and hidden verification constraints (GC, PC, LG, MM, SN, SQ), pp. 1686–1691.
DATEDATE-2009-HeH #algorithm #encoding #performance #verification
An efficient path-oriented bitvector encoding width computation algorithm for bit-precise verification (NH, MSH), pp. 1602–1607.
DATEDATE-2009-LettninNBRGKRSR #hardware #verification
Semiformal verification of temporal properties in automotive hardware dependent software (DL, PKN, JB, JR, JG, TK, WR, VS, SR), pp. 1214–1217.
DATEDATE-2009-RichterJE #framework #learning #verification
Learning early-stage platform dimensioning from late-stage timing verification (KR, MJ, RE), pp. 851–857.
DocEngDocEng-2009-SchonbergWJF #documentation #verification
Logic-based verification of technical documentation (CS, FW, MJ, BF), pp. 251–252.
DRRDRR-2009-LiD #difference #independence #using #verification
Improving semi-text-independent method of writer verification using difference vector (XL, XD), pp. 1–10.
DRRDRR-2009-SrihariB #comparison #modelling #statistics #verification
Comparison of statistical models for writer verification (SNS, GRB), pp. 1–10.
ICDARICDAR-2009-Alonso-FernandezFGGO #robust #verification
Robustness of Signature Verification Systems to Imitators with Increasing Skills (FAF, JF, AG, JG, JOG), pp. 728–732.
ICDARICDAR-2009-BatistaGS #approach #multi #verification
A Multi-Hypothesis Approach for Off-Line Signature Verification with HMMs (LB, EG, RS), pp. 1315–1319.
ICDARICDAR-2009-BlankersHFV #contest #verification
ICDAR 2009 Signature Verification Competition (VLB, CEvdH, KF, LV), pp. 1403–1407.
ICDARICDAR-2009-BonillaFGH #pseudo #verification
Offline Signature Verification Based on Pseudo-Cepstral Coefficients (JFVB, MAFB, CMTG, JBAH), pp. 126–130.
ICDARICDAR-2009-GalballyFMO #evaluation #using #verification
Evaluation of Brute-force Attack to Dynamic Signature Verification Using Synthetic Samples (JG, JF, MMD, JOG), pp. 131–135.
ICDARICDAR-2009-IbrahimKKAG #analysis #dependence #online #using #verification
On-Line Signature Verification: Directional Analysis of a Signature Using Weighted Relative Angle Partitions for Exploitation of Inter-Feature Dependencies (MTI, MJK, MAK, KSA, LG), pp. 41–45.
ICDARICDAR-2009-NguyenBL #problem #verification
Global Features for the Off-Line Signature Verification Problem (VN, MB, GL), pp. 1300–1304.
ICDARICDAR-2009-PrakashG #geometry #verification
Geometric Centroids and their Relative Distances for Off-line Signature Verification (HNP, DSG), pp. 121–125.
ICDARICDAR-2009-WangHL #verification
A New Block Partitioned Text Feature for Text Verification (XW, LH, CL), pp. 366–370.
VLDBVLDB-2009-PangZM #database #outsourcing #scalability #verification
Scalable Verification for Outsourced Dynamic Databases (HP, JZ, KM), pp. 802–813.
ESOPESOP-2009-KikuchiK #authentication #automation #encryption #protocol #type system #verification
Type-Based Automated Verification of Authenticity in Cryptographic Protocols (DK, NK), pp. 222–236.
ESOPESOP-2009-RajanTSL #composition #design #named #policy #verification #web #web service
Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services (HR, JT, SMS, GTL), pp. 333–347.
FASEFASE-2009-BoronatHM #logic #model transformation #semantics #verification
Rewriting Logic Semantics and Verification of Model Transformations (AB, RH, JM), pp. 18–33.
FASEFASE-2009-GiannakopoulouP #composition #generative #interface #verification
Interface Generation and Compositional Verification in JavaPathfinder (DG, CSP), pp. 94–108.
FASEFASE-2009-Sery #specification #verification
Enhanced Property Specification and Verification in BLAST (OS), pp. 456–469.
TACASTACAS-2009-BrughNR #dot-net #named #source code #verification
MoonWalker: Verification of .NET Programs (NHMAdB, VYN, TCR), pp. 170–173.
TACASTACAS-2009-ChenFCTW #automaton #composition #learning #verification
Learning Minimal Separating DFA’s for Compositional Verification (YFC, AF, EMC, YKT, BYW), pp. 31–45.
TACASTACAS-2009-YuBI #analysis #string #verification
Symbolic String Verification: Combining String Analysis and Size Analysis (FY, TB, OHI), pp. 322–336.
PLDIPLDI-2009-KawaguchiRJ #data type #type system #verification
Type-based data structure verification (MK, PMR, RJ), pp. 304–315.
PLDIPLDI-2009-SrivastavaG #abstraction #using #verification
Program verification using templates over predicate abstraction (SS, SG), pp. 223–234.
SASSAS-2009-Qadeer #algorithm #smt #using #verification
Algorithmic Verification of Systems Software Using SMT Solvers (SQ), p. 2.
ICALPICALP-v2-2009-Boldo #case study #float #verification
Floats and Ropes: A Case Study for Formal Numerical Program Verification (SB), pp. 91–102.
FMFM-2009-AlpuenteBR #logic #specification #verification #web
Specification and Verification of Web Applications in Rewriting Logic (MA, DB, DR), pp. 790–805.
FMFM-2009-LeuschelFFP #automation #modelling #scalability #verification
Automated Property Verification for Large Scale B Models (ML, JF, FF, DP), pp. 708–723.
FMFM-2009-LuthW #c #source code #specification #verification
Certifiable Specification and Verification of C Programs (CL, DW), pp. 419–434.
FMFM-2009-PlatzerC #case study #verification
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study (AP, EMC), pp. 547–562.
FMFM-2009-Rajamani #statistics #testing #verification
Verification, Testing and Statistics (SKR), pp. 33–40.
FMFM-2009-SouyrisWDD #verification
Formal Verification of Avionics Software Products (JS, VW, DD, HD), pp. 532–546.
IFMIFM-2009-BuiN #random #verification
Formal Verification Based on Guided Random Walks (THB, AN), pp. 72–87.
IFMIFM-2009-LangariT #graph transformation #verification
Application of Graph Transformation in Verification of Dynamic Systems (ZL, RJT), pp. 261–276.
SEFMSEFM-2009-BersaniFPR #modelling #multi #paradigm #realtime #verification
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms (MMB, CAF, MP, MR), pp. 13–22.
SEFMSEFM-2009-Chalin #verification
Adjusted Verification Rules for Loops Are More Complete and Give Better Diagnostics for Less (PC), pp. 317–324.
SEFMSEFM-2009-Jeannet #concurrent #interprocedural #relational #source code #verification
Relational Interprocedural Verification of Concurrent Programs (BJ), pp. 83–92.
SEFMSEFM-2009-Rushby #assurance #verification
Software Verification and System Assurance (JMR), pp. 3–10.
SEFMSEFM-2009-TatsutaCA #logic #pointer #verification
Completeness of Pointer Program Verification by Separation Logic (MT, WNC, MFAA), pp. 179–188.
AdaEuropeAdaEurope-2009-BerthomieuBCDFV #specification #verification
Formal Verification of AADL Specifications in the Topcased Environment (BB, JPB, CC, SDZ, MF, FV), pp. 207–221.
AdaSIGAda-2009-Knight #ada #approach #named #verification
Echo: a new approach to formal verification based on Ada (JK), pp. 85–86.
CAiSECAiSE-2009-LiuLYWH #analysis #constraints #using #verification #workflow
ETL Workflow Analysis and Verification Using Backwards Constraint Propagation (JL, SL, DY, JW, TH), pp. 455–469.
EDOCEDOC-2009-BoukhebouzeABM #modelling #process #rule-based #using #verification
Rule-Based Modeling and Verification of Business Processes Using ECAPE Net (MB, YA, ANB, ZM), p. 74–?.
ICEISICEIS-HCI-2009-NakanishiTO #artificial reality #complexity #design #effectiveness #guidelines #using #verification
Study for Establishing Design Guidelines for Manuals using Augmented Reality Technology — Verification and Expansion of the Basic Model Describing “Effective Complexity” (MN, SiT, YO), pp. 21–26.
ICEISICEIS-J-2009-MoralesC #automation #composition #process #verification
Automatic Compositional Verification of Business Processes (LEMM, MIC), pp. 479–490.
SEKESEKE-2009-ShahrokniFPB #challenge #robust #verification
Robustness Verification Challenges in Automotive Telematics Software (AS, RF, FP, AB), pp. 460–465.
SEKESEKE-2009-YuanHZL #automation #modelling #multi #transaction #verification
Modeling and Verification of Automatic Multi-business Transactions (MY, ZH, JZ, XL), pp. 274–279.
SEKESEKE-2009-ZhangLSDCL #scalability #verification
Formal Verification of Scalable NonZero Indicators (SJZ, YL, JS, JSD, WC, YAL), pp. 406–411.
MODELSMoDELS-2009-KraemerH #automation #development #encapsulation #incremental #process #uml #verification
Automated Encapsulation of UML Activities for Incremental Development and Verification (FAK, PH), pp. 571–585.
MODELSMoDELS-2009-KraemerH #automation #development #encapsulation #incremental #process #uml #verification
Automated Encapsulation of UML Activities for Incremental Development and Verification (FAK, PH), pp. 571–585.
PPDPPPDP-2009-Virseda #algorithm #debugging #declarative #framework #higher-order #logic #source code #verification
A higher-order logical framework for the algorithmic debugging and verification of declarative programs (RdVV), pp. 49–60.
PADLPADL-2009-WangBLS #declarative #network #verification
Declarative Network Verification (AW, PB, BTL, OS), pp. 61–75.
POPLPOPL-2009-HawblitzelP #automation #garbage collection #verification
Automated verification of practical garbage collectors (CH, EP), pp. 441–453.
POPLPOPL-2009-Kobayashi #higher-order #recursion #source code #verification
Types and higher-order recursion schemes for verification of higher-order programs (NK), pp. 416–428.
RERE-2009-Hall #forensics #verification
Forensic System Verification (RJH), pp. 111–120.
RERE-2009-PostSMGK #functional #requirements #verification
Linking Functional Requirements and Software Verification (HP, CS, FM, TG, TK), pp. 295–302.
RERE-2009-SalinesiRDM #classification #fault #feature model #modelling #product line #towards #verification
Looking for Product Line Feature Models Defects: Towards a Systematic Classification of Verification Criteria (CS, CR, DD, RM), pp. 385–386.
SACSAC-2009-BaechlerBH #image #modelling #using #verification
Labeled images verification using Gaussian mixture models (MB, JLB, JH), pp. 1331–1335.
SACSAC-2009-BeekMG #framework #named #verification
CMC-UMC: a framework for the verification of abstract service-oriented properties (MHtB, FM, SG), pp. 2111–2117.
SACSAC-2009-GiroD #automaton #on the #probability #verification
On the verification of probabilistic I/O automata with unspecified rates (SG, PRD), pp. 582–586.
SACSAC-2009-RodriguesSC #composition #embedded #functional #set #using #verification
Improving functional verification of embedded systems using hierarchical composition and set theory (CLR, KRGdS, HdNC), pp. 1632–1636.
SACSAC-2009-SharyginaTT #abstraction #performance #precise #verification
The synergy of precise and fast abstractions for program verification (NS, ST, AT), pp. 566–573.
SACSAC-2009-SongKS #approach #aspect-oriented #modelling #verification
A property-based verification approach in aspect-oriented modeling (ES, HK, WS), pp. 545–546.
ESEC-FSEESEC-FSE-2009-BozzanoCRKNN #evaluation #modelling #performance #verification
Verification and performance evaluation of aadl models (MB, AC, MR, JPK, VYN, TN), pp. 285–286.
ESEC-FSEESEC-FSE-2009-HannaBR #automation #automaton #behaviour #composition #independence #verification
Behavioral automata composition for automatic topology independent verification of parameterized systems (YH, SB, HR), pp. 325–334.
HPCAHPCA-2009-ChenLHCSWP #consistency #memory management #performance #verification
Fast complete memory consistency verification (YC, YL, WH, TC, HS, PW, HP), pp. 381–392.
LCTESLCTES-2009-AndreM #requirements #specification #verification
Specification and verification of time requirements with CCSL and Esterel (CA, FM), pp. 167–176.
PPoPPPPoPP-2009-VoVDGKT #source code #verification
Formal verification of practical MPI programs (AV, SSV, MD, GG, RMK, RT), pp. 261–270.
SOSPSOSP-2009-KleinEHACDEEKNSTW #kernel #named #verification
seL4: formal verification of an OS kernel (GK, KE, GH, JA, DC, PD, DE, KE, RK, MN, TS, HT, SW), pp. 207–220.
CADECADE-2009-PlatzerQR #verification
Real World Verification (AP, JDQ, PR), pp. 485–501.
CAVCAV-2009-BensalemBNS #composition #concurrent #detection #named #verification
D-Finder: A Tool for Compositional Deadlock Detection and Verification (SB, MB, THN, JS), pp. 614–619.
CAVCAV-2009-BozgaHIKV #array #automation #integer #source code #verification
Automatic Verification of Integer Array Programs (MB, PH, RI, FK, TV), pp. 157–172.
CAVCAV-2009-HuntS #verification
Centaur Technology Media Unit Verification (WAHJ, SS), pp. 353–367.
CAVCAV-2009-KaivolaGNTWPSTFRN #execution #testing #validation #verification
Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation (RK, RG, NN, AT, JW, SP, AS, CT, VF, ER, AN), pp. 414–429.
CAVCAV-2009-Kim #performance #verification
Mixed-Signal System Verification: A High-Speed Link Example (JK), p. 16.
CAVCAV-2009-LomuscioQR #model checking #multi #named #verification
MCMAS: A Model Checker for the Verification of Multi-Agent Systems (AL, HQ, FR), pp. 682–688.
CAVCAV-2009-SrivastavaGF #named #smt #verification
VS3: SMT Solvers for Program Verification (SS, SG, JSF), pp. 702–708.
CAVCAV-2009-Strichman #equivalence #proving #source code #verification
Regression Verification: Proving the Equivalence of Similar Programs (OS), p. 63.
CAVCAV-2009-SunLDP #flexibility #named #towards #verification
PAT: Towards Flexible Verification under Fairness (JS, YL, JSD, JP), pp. 709–714.
ICLPICLP-2009-MeraLH #framework #runtime #testing #verification
Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework (EM, PLG, MVH), pp. 281–295.
TAPTAP-2009-HerberFG #model checking #process #testing
Combining Model Checking and Testing in a Continuous HW/SW Co-verification Process (PH, FF, SG), pp. 121–136.
TAPTAP-2009-NoriR #statistics #testing #verification
Verification, Testing and Statistics (AVN, SKR), pp. 6–9.
VMCAIVMCAI-2009-Cortier #protocol #security #verification
Verification of Security Protocols (VC), pp. 5–13.
CBSECBSE-2008-ChoiB #component #design #towards #verification
Towards Component-Based Design and Verification of a µ-Controller (YC, CB), pp. 196–211.
ECSAECSA-2008-Atkinson #architecture #component #testing #verification
Component-Oriented Verification of Software Architectures through Built-in Tests (CA), p. 2.
ASEASE-2008-BordiniDFF #automation #multi #source code #verification
Automated Verification of Multi-Agent Programs (RHB, LAD, BF, MF), pp. 69–78.
ASEASE-2008-BordinPP #agile #modelling #prototype #realtime #verification
Rapid Model-Driven Prototyping and Verification of High-Integrity Real-Time Systems (MB, MP, SP), pp. 491–492.
ASEASE-2008-HolzmannJG #verification
Swarm Verification (GJH, RJ, AG), pp. 1–6.
ASEASE-2008-IspirC #aspect-oriented #programming #verification
An Assume Guarantee Verification Methodology for Aspect-Oriented Programming (MI, ABC), pp. 391–394.
ASEASE-2008-PostS #verification
Configuration Lifting: Verification meets Software Configuration (HP, CS), pp. 347–350.
CASECASE-2008-BenedettoDSW #automation #mining #verification
Automatic verification of wireless control in a mining ventilation system (MDDB, AD, ES, EW), pp. 858–863.
CASECASE-2008-LjungkrantzAF #component #industrial #logic #programming #specification #verification
Formal specification and verification of components for industrial logic control programming (OL, , MF), pp. 935–940.
CASECASE-2008-ZhangMT #rule-based #verification
Verification of ECA rule based management and control systems (JZ, JRM, DMT), pp. 1–7.
DACDAC-2008-Beers #experience #verification
Pre-RTL formal verification: an intel experience (RB), pp. 806–811.
DACDAC-2008-Cummings #design #verification
SystemVerilog implicit port enhancements accelerate system design & verification (CEC), pp. 231–236.
DACDAC-2008-HaldarSPDG #c++ #modelling #verification
Construction of concrete verification models from C++ (MH, GS, SP, BD, AG), pp. 942–947.
DACDAC-2008-HoTDDGS #identification #logic #verification
Early formal verification of conditional coverage points to identify intrinsically hard-to-verify logic (RCH, MT, MMD, ROD, JG, DES), pp. 268–271.
DACDAC-2008-LiZY #analysis #verification
Full-chip leakage analysis in nano-scale technologies: mechanisms, variation sources, and verification (TL, WZ, ZY), pp. 594–599.
DACDAC-2008-MenezesKA #grid #power management #verification
A “true” electrical cell model for timing, noise, and power grid verification (NM, CVK, CSA), pp. 462–467.
DACDAC-2008-Mitra #verification
Strategies for mainstream usage of formal verification (RSM), pp. 800–805.
DACDAC-2008-Moon #composition #optimisation #verification
Compositional verification of retiming and sequential optimizations (IHM), pp. 131–136.
DACDAC-2008-Ng #challenge #modelling #using #verification
Challenges in using system-level models for RTL verification (KN), pp. 812–815.
DACDAC-2008-SenOA #multi #predict #runtime #verification
Predictive runtime verification of multi-processor SoCs in SystemC (AS, VO, MSA), pp. 948–953.
DACDAC-2008-TurumellaS #concurrent #thread #verification
Assertion-based verification of a 32 thread SPARCTM CMT microprocessor (BT, MS), pp. 256–261.
DATEDATE-2008-ChengH #invariant #mining #verification
Simulation-Directed Invariant Mining for Software Verification (XC, MSH), pp. 682–687.
DATEDATE-2008-FreuerJGN #constraints #design #higher-order #on the #verification
On the Verification of High-Order Constraint Compliance in IC Design (JBF, GJ, JG, WN), pp. 26–31.
DATEDATE-2008-LaiHK #identification #multi #verification
Improving Constant-Coefficient Multiplier Verification by Partial Product Identification (CYL, CYH, KYK), pp. 813–818.
DATEDATE-2008-LettninNRKRKSR #embedded #verification
Verification of Temporal Properties in Automotive Embedded Software (DL, PKN, JR, TK, WR, TK, VS, SR), pp. 164–169.
DATEDATE-2008-WagnerB #adaptation #design #manycore #named #verification
MCjammer: Adaptive Verification for Multi-core Designs (IW, VB), pp. 670–675.
DATEDATE-2008-WeinbergerBB #design #modelling #petri net #process #verification #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.
DRRDRR-2008-BrinkKS #automation #identification #verification
Automatic removal of crossed-out handwritten text and the effect on writer verification and identification (AB, HvdK, LS), p. 68150.
VLDBVLDB-2008-ShangZLY #algorithm #morphism #performance #testing #verification
Taming verification hardness: an efficient algorithm for testing subgraph isomorphism (HS, YZ, XL, JXY), pp. 364–375.
ESOPESOP-2008-LeinoM #verification
Verification of Equivalent-Results Methods (KRML, PM), pp. 307–321.
ESOPESOP-2008-Ong #approach #higher-order #semantics #verification
Verification of Higher-Order Computation: A Game-Semantic Approach (CHLO), pp. 299–306.
FASEFASE-2008-BisztrayHE #architecture #refactoring #verification
Verification of Architectural Refactorings by Rule Extraction (DB, RH, HE), pp. 347–361.
FASEFASE-2008-CiobanuK #interactive #migration #modelling #verification
Modelling and Verification of Timed Interaction and Migration (GC, MK), pp. 215–229.
TACASTACAS-2008-AlkassarSS #pervasive #verification
Formal Pervasive Verification of a Paging Mechanism (EA, NS, AS), pp. 109–123.
TACASTACAS-2008-FarzanCCTW #automation #composition #regular expression #verification
Extending Automated Compositional Verification to the Full Class of ω-Regular Languages (AF, YFC, EMC, YKT, BYW), pp. 2–17.
TACASTACAS-2008-IhlemannJS #on the #reasoning #verification
On Local Reasoning in Verification (CI, SJ, VSS), pp. 265–281.
TACASTACAS-2008-LegayMOW #automation #on the #probability #source code #verification
On Automated Verification of Probabilistic Programs (AL, ASM, JO, JW), pp. 173–187.
TACASTACAS-2008-Malik #hardware #verification
Hardware Verification: Techniques, Methodology and Solutions (SM), p. 1.
TACASTACAS-2008-SaksenaWJ #ad hoc #graph grammar #modelling #protocol #verification
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols (MS, OW, BJ), pp. 18–32.
TACASTACAS-2008-WahlBE #named #symmetry #verification
SVISS: Symbolic Verification of Symmetric Systems (TW, NB, EAE), pp. 459–462.
CSMRCSMR-2008-LiTLMC #requirements #validation #verification
Coping with Requirements Changes in Software Verification and Validation (SL, LT, WL, MM, GC), pp. 317–318.
PEPMPEPM-2008-PietrzakCPH #analysis #composition #prolog #source code #verification
A practical type analysis for verification of modular prolog programs (PP, JC, GP, MVH), pp. 61–70.
PEPMPEPM-2008-SultanaT #refactoring #verification
Mechanical verification of refactorings (NS, SJT), pp. 51–60.
PLDIPLDI-2008-ZeeKR #data type #functional #linked data #open data #verification
Full functional verification of linked data structures (KZ, VK, MCR), pp. 349–361.
ICALPICALP-B-2008-BrazdilFK #branch #markov #process #synthesis #verification
Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives (TB, VF, AK), pp. 148–159.
FMFM-2008-ArvindDK #design #verification
Getting Formal Verification into Design Flow (A, ND, MK), pp. 12–32.
FMFM-2008-EmmiGP #automaton #interface #verification
Assume-Guarantee Verification for Interface Automata (ME, DG, CSP), pp. 116–131.
FMFM-2008-FuriaPR #approximate #automation #specification #verification
Automated Verification of Dense-Time MTL Specifications Via Discrete-Time Approximation (CAF, MP, MR), pp. 132–147.
FMFM-2008-GrandyBSSR #protocol #security #verification
Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code (HG, MB, KS, GS, WR), pp. 165–180.
SEFMSEFM-2008-BartheKPS #hybrid #proving #verification
Preservation of Proof Pbligations for Hybrid Verification Methods (GB, CK, DP, JSF), pp. 127–136.
SEFMSEFM-2008-Gladisch #branch #generative #testing
Verification-Based Test Case Generation for Full Feasible Branch Coverage (CG), pp. 159–168.
SEFMSEFM-2008-QuintonG #component #contract #verification
Contract-Based Verification of Hierarchical Systems of Components (SQ, SG), pp. 377–381.
SEFMSEFM-2008-SchaeferP #adaptation #composition #embedded #modelling #reasoning #verification
Compositional Reasoning in Model-Based Verification of Adaptive Embedded Systems (IS, APH), pp. 95–104.
SEFMSEFM-2008-XavierHM #fault tolerance #source code #using #verification
Using Formal Verification to Reduce Test Space of Fault-Tolerant Programs (KSX, SH, ACVdM), pp. 181–190.
GT-VMTGT-VMT-2008-BucchiaroneG #architecture #using #verification
Dynamic Software Architectures Verification using DynAlloy (AB, JPG).
GT-VMTGT-VMT-2008-KumarM #automaton #sequence chart #verification
Improving Live Sequence Chart to Automata Transformation for Verification (RK, EGM).
ICGTICGT-2008-Aalst #consistency #verification #workflow
Discovery, Verification and Conformance of Workflows with Cancellation (WMPvdA), pp. 18–37.
ICGTICGT-2008-Bisztray #architecture #refactoring #tool support #verification
Verification of Architectural Refactorings: Rule Extraction and Tool Support (DB), pp. 475–477.
ICGTICGT-2008-Horvath #approach #graph transformation #towards #verification
Towards a Two Layered Verification Approach for Compiled Graph Transformation (ÁH), pp. 499–501.
ICGTICGT-2008-KonigK #graph transformation #towards #verification
Towards the Verification of Attributed Graph Transformation Systems (BK, VK), pp. 305–320.
AdaEuropeAdaEurope-2008-OberH #on the #verification
On the Timed Automata-Based Verification of Ravenscar Systems (IO, NH), pp. 30–43.
ICEISICEIS-DISI-2008-SalemGB #concept #modelling #multi #specification #verification
Multi-Dimensional Modeling — Formal Specification and Verification of the Hierarchy Concept (AS, FG, HBA), pp. 317–322.
ICEISICEIS-ISAS1-2008-MoralesTPA #communication #composition #concept #model checking #verification
A Conceptual Scheme for Compositional Model-Checking Verification of Critical Communicating Systems (LEMM, MICT, MAP, KBA), pp. 86–93.
ICEISICEIS-ISAS2-2008-BainaT #algorithm #graph #hybrid #towards #verification #workflow
Toward a Hybrid Algorithm for Workflow Graph Structural Verification (FT, KB, WG), pp. 442–447.
ICEISICEIS-ISAS2-2008-TobarraCPC #protocol #verification
Formal Verification of the Secure Sockets Layer Protocol (MLT, DC, JJP, FC), pp. 246–252.
ICEISICEIS-J-2008-MoralesCPA #composition #model checking #verification
Compositional Model-Checking Verification of Critical Systems (LEMM, MIC, MAP, KBA), pp. 213–225.
ICPRICPR-2008-IbrahimG #online #using #verification
On-line signature verification by using most discriminating points (MTI, LG), pp. 1–4.
ICPRICPR-2008-LiuW #online #verification
Template selection for on-line signature verification (NL, YW), pp. 1–4.
ICPRICPR-2008-MottlLSY #kernel #online #verification
Signature verification based on fusion of on-line and off-line kernels (VM, ML, VS, AY), pp. 1–4.
ICPRICPR-2008-NeebaJ #recognition #verification
Recognition of books by verification and retraining (NVN, CVJ), pp. 1–4.
SEKESEKE-2008-ChenLMW #algorithm #case study #optimisation #polynomial #problem #verification
Verification of Optimization Algorithms: a Case Study of a Quadratic Assignment Problem Solver (TYC, HL, RGM, DW), pp. 16–21.
SEKESEKE-2008-GarciaRS #automation #ltl #named #verification
PROTEF: Automatic Verification of Pattern-Based LTL Templates (LG, SR, SS), pp. 261–266.
SEKESEKE-2008-KloukinasSM #distributed #runtime #verification
Estimating Event Lifetimes for Distributed Runtime Verification (CK, GS, KM), pp. 117–122.
SEKESEKE-2008-NakaoaTM #case study #independence #validation #verification
Estimating the Effort of Independent Verification and Validation in the Context of Mission-critical Software Systems — A Case Study (HN, AT, JM), pp. 167–172.
SEKESEKE-2008-Shaffer #domain model #security #source code #static analysis #verification
A Security Domain Model for Static Analysis and Verification of Software Programs (ABS), pp. 673–678.
ECOOPECOOP-2008-DrossopoulouFMS #framework #invariant #verification
A Unified Framework for Verification Techniques for Object Invariants (SD, AF, PM, AJS), pp. 412–437.
OOPSLAOOPSLA-2008-DistefanoP #java #named #towards #verification
jStar: towards practical verification for java (DD, MJP), pp. 213–226.
PPDPPPDP-2008-Leuschel #declarative #programming #verification
Declarative programming for verification: lessons and outlook (ML), pp. 1–7.
POPLPOPL-2008-ChinDNQ #composition #logic #object-oriented #verification
Enhancing modular OO verification with separation logic (WNC, CD, HHN, SQ), pp. 87–99.
POPLPOPL-2008-LahiriQ #precise #smt #using #verification
Back to the future: revisiting precise program verification using SMT solvers (SKL, SQ), pp. 171–182.
POPLPOPL-2008-TristanL #case study #optimisation #scheduling #validation #verification
Formal verification of translation validators: a case study on instruction scheduling optimizations (JBT, XL), pp. 17–27.
REFSQREFSQ-2008-MarincicMW #embedded #requirements #verification
Classifying Assumptions Made during Requirements Verification of Embedded Systems (JM, AM, RW), pp. 141–146.
SACSAC-2008-BaF #composition #dependence #graph #web #web service
Dependence graphs for verifications of web service compositions with PEWS (CB, MHF), pp. 2387–2391.
SACSAC-2008-HojjatMS #algebra #evaluation #framework #functional #performance #probability #process #verification
A framework for performance evaluation and functional verification in stochastic process algebras (HH, MRM, MS), pp. 339–346.
SACSAC-2008-LiQWLW #consistency #diagrams #interactive #java #runtime #source code #state machine #uml #verification
UML state machine diagram driven runtime verification of Java programs for message interaction consistency (XL, XQ, LW, BL, WEW), pp. 384–389.
SACSAC-2008-MeloNX #java #source code #testing #towards #verification
Towards verification and testing of Java programs (ACVdM, PRFN, KSX), pp. 730–734.
SACSAC-2008-ShiYLZ #composition #semantics #verification #web #web service
Path-based verification for composition of semantic web services (YS, JY, ZJL, JZ), pp. 2392–2396.
FSEFSE-2008-YuWGB #composition #encoding #performance #summary #using #verification #web #web service
Modular verification of web services using efficient symbolic encoding and summarization (FY, CW, AG, TB), pp. 192–202.
ICSEICSE-2008-BeekGKM #verification
Formal verification of an automotive scenario in service-oriented computing (MHtB, SG, NK, FM), pp. 613–622.
ICSEICSE-2008-ChenDS #calculus #verification
A verification system for timed interval calculus (CC, JSD, JS), pp. 271–280.
ICSEICSE-2008-ChenY #constraints #dependence #grid #verification #workflow
Temporal dependency based checkpoint selection for dynamic verification of fixed-time constraints in grid workflow systems (JC, YY), pp. 141–150.
CCCC-2008-MalePPD #bytecode #java #verification
Java Bytecode Verification for @NonNull Types (CM, DJP, AP, CD), pp. 229–244.
CAVCAV-2008-BaswanaMP #consistency #memory management #set #verification
Implied Set Closure and Its Application to Memory Consistency Verification (SB, SKM, VP), pp. 94–106.
CAVCAV-2008-BurckhardtM #effectiveness #memory management #modelling #verification
Effective Program Verification for Relaxed Memory Models (SB, MM), pp. 107–120.
CAVCAV-2008-CohenPZ #memory management #transaction #verification
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses (AC, AP, LDZ), pp. 121–134.
CAVCAV-2008-Cremers #analysis #protocol #security #verification
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols (CJFC), pp. 414–418.
CAVCAV-2008-EisnerNY #composition #design #functional #power management #reasoning #verification
Functional Verification of Power Gated Designs by Compositional Reasoning (CE, AN, KY), pp. 433–445.
CAVCAV-2008-Foster #industrial #tutorial #verification
Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial) (HF), pp. 5–10.
CAVCAV-2008-Harrison #proving #theorem proving #tutorial #verification
Theorem Proving for Verification (Invited Tutorial) (JH), pp. 11–18.
CAVCAV-2008-JoshiK #graph transformation #theorem #verification
Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems (SJ, BK), pp. 214–226.
CAVCAV-2008-MeikleF #approach #proving #verification
Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B (LIM, JDF), pp. 309–313.
CAVCAV-2008-NguyenC #verification
Enhancing Program Verification with Lemmas (HHN, WNC), pp. 355–369.
CAVCAV-2008-VakkalankaGK #order #reduction #source code #verification
Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings (SSV, GG, RMK), pp. 66–79.
ICLPICLP-2008-MontaliTACGLM #declarative #logic programming #specification #using #verification
Verification from Declarative Specifications Using Logic Programming (MM, PT, MA, FC, MG, EL, PM), pp. 440–454.
ICSTICST-2008-UbayashiPST #aspect-oriented #contract #refactoring #verification
Contract-Based Verification for Aspect-Oriented Refactoring (NU, JP, SS, TT), pp. 180–189.
IJCARIJCAR-2008-Comon-Lundh #automation #challenge #protocol #security #verification
Challenges in the Automated Verification of Security Protocols (HCL), pp. 396–409.
IJCARIJCAR-2008-Gupta #automation #challenge #verification
Software Verification: Roles and Challenges for Automatic Decision Procedures (AG), p. 1.
TAPTAP-2008-EngelGKR #object-oriented #testing #verification
Integrating Verification and Testing of Object-Oriented Software (CE, CG, VK, PR), pp. 182–191.
TAPTAP-2008-Hennell #experience #verification
The First Thirty Years: Experience with Software Verification (MAH), pp. 1–3.
FATESTestCom-FATES-2008-GrozLPS #analysis #composition #reachability #testing #verification
Modular System Verification by Inference, Testing and Reachability Analysis (RG, KL, AP, MS), pp. 216–233.
FATESTestCom-FATES-2008-Havelund #c #runtime #source code #verification
Runtime Verification of C Programs (KH), pp. 7–22.
VMCAIVMCAI-2008-Goldberg #on the #simulation #verification
On Bridging Simulation and Formal Verification (EG), pp. 127–141.
VMCAIVMCAI-2008-Palsberg #verification
Verification of Register Allocators (JP), p. 6.
CBSECBSE-2007-BaiWDTC #collaboration #contract #framework #validation #verification #web #web service
A Framework for Contract-Based Collaborative Verification and Validation of Web Services (XB, YW, GD, WTT, YC), pp. 258–273.
ECSAECSA-2007-JeradBG #architecture #maude #verification
Hierarchical Verification in Maude of L f P Software Architectures (CJ, KB, AGT), pp. 156–170.
ASEASE-2007-BarlasB #distributed #framework #java #named #verification
Netstub: a framework for verification of distributed java applications (EB, TB), pp. 24–33.
ASEASE-2007-CabotCR #constraints #modelling #named #ocl #programming #uml #using #verification
UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming (JC, RC, DR), pp. 547–548.
CASECASE-2007-AnLM #collaboration #design #verification
Expression and Verification of Task Management in Collaborative Design (YSA, RHL, AM), pp. 800–805.
CASECASE-2007-ReveliotisR0 #algebra #concurrent #correctness #policy #programming #verification
Correctness Verification of Generalized Algebraic Deadlock Avoidance Policies through Mathematical Programming (SR, ER, JYC), pp. 200–206.
CASECASE-2007-YangM #approach #automation #feature model #interactive #matrix #verification
Automatic Feasibility Verification of Object Configurations: A New Approach Based on Feature Interaction Matrices (FY, MMM), pp. 686–691.
DACDAC-2007-BacchiniHFRLTPZ #question #verification
Verification Coverage: When is Enough, Enough? (FB, AJH, TF, RR, DL, MT, AP, AZ), pp. 744–745.
DACDAC-2007-KasuyaT #design #verification
Verification Methodologies in a TLM-to-RTL Design Flow (AK, TT), pp. 199–204.
DACDAC-2007-LongS #verification
Synthesizing SVA Local Variables for Formal Verification (JL, AS), pp. 75–80.
DACDAC-2007-MathurK #design #modelling #verification
Design for Verification in System-level Models and RTL (AM, VK), pp. 193–198.
DACDAC-2007-PetlinS #functional #multi #verification
Functional Verification of SiCortex Multiprocessor System-on-a-Chip (OP, WS), pp. 906–909.
DACDAC-2007-Vardi #verification
Formal Techniques for SystemC Verification; Position Paper (MYV), pp. 188–192.
DACDAC-2007-YangHH #automation #behaviour #design #verification
Automatic Verification of External Interrupt Behaviors for Microprocessor Design (FCY, WKH, IJH), pp. 896–901.
DATEDATE-2007-Al-SammaneZT #design #verification
A symbolic methodology for the verification of analog and mixed signal designs (GAS, MHZ, ST), pp. 249–254.
DATEDATE-2007-BronckersSPVR #analysis #interactive #simulation #verification
Interactive presentation: Simulation methodology and experimental verification for the analysis of substrate noise on LC-VCO’s (SB, CS, GVdP, GV, YR), pp. 1520–1525.
DATEDATE-2007-LeGB #pervasive #verification
Formal verification of a pervasive interconnect bus system in a high-performance microprocessor (TL, TG, JB), pp. 219–224.
DATEDATE-2007-LisselGG #design #industrial #perspective #verification
Introducing new verification methods into a company’s design flow: an industrial user’s point of view (RL, JG), pp. 689–694.
DATEDATE-2007-SeshiaLM #fault
Verification-guided soft error resilience (SAS, WL, SM), pp. 1442–1447.
ICDARICDAR-2007-AraujoCF #approach #online #verification
An Approach to Improve Accuracy Rate of On-line Signature Verification Systems of Different Sizes (RA, GDCC, ECBCF), pp. 332–336.
ICDARICDAR-2007-BhardwajSSS #on the #verification
On the Use of Lexeme Features for Writer Verification (AB, AS, HS, SNS), pp. 1088–1092.
ICDARICDAR-2007-BrinkSB #identification #towards #using #verification
Towards Explainable Writer Verification and Identification Using Vantage Writers (AB, LS, MB), pp. 824–828.
ICDARICDAR-2007-BulacuSB #identification #independence #verification
Text-Independent Writer Identification and Verification on Offline Arabic Handwriting (MB, LS, AB), pp. 769–773.
ICDARICDAR-2007-ChangS #online #verification
Modified Dynamic Time Warping for Stroke-Based On-line Signature Verification (WC, JS), pp. 724–728.
ICDARICDAR-2007-CoetzerS #verification
A Human-Centric Off-Line Signature Verification System (HC, RS), pp. 153–157.
ICDARICDAR-2007-HummIH #modelling #statistics #using #verification
Spoken Handwriting Verification Using Statistical Models (AH, RI, JH), pp. 999–1003.
ICDARICDAR-2007-Martinez-DiazFFO #on the #verification
On The Effects of Sampling Rate and Interpolation in HMM-Based Dynamic Signature Verification (MMD, JFA, MRF, JOG), pp. 1113–1117.
ICDARICDAR-2007-NejadR #identification #verification
A New Method for Writer Identification and Verification Based on Farsi/Arabic Handwritten Texts (FN, MR), pp. 829–833.
ICDARICDAR-2007-NguyenBML #classification #using #verification
Off-line Signature Verification Using Enhanced Modified Direction Features in Conjunction with Neural Classifiers and Support Vector Machines (VN, MB, VM, GL), pp. 734–738.
ICDARICDAR-2007-PapavassiliouSKC #parametricity #verification
A Parametric Spectral-Based Method for Verification of Text in Videos (VP, TS, VK, GC), pp. 879–883.
ICDARICDAR-2007-Schomaker07a #identification #roadmap #verification
Advances in Writer Identification and Verification (LS), pp. 1268–1273.
ICDARICDAR-2007-SrinivasanKHS #on the #verification
On Computing Strength of Evidence for Writer Verification (HS, SK, CH, SNS), pp. 844–848.
ICDARICDAR-2007-VargasFTA07a #image #performance #verification
Off-line Signature Verification System Performance against Image Acquisition Resolution (JFVB, MAFB, CMTG, JBA), pp. 834–838.
SIGMODSIGMOD-2007-ChengKNL #database #graph #named #query #towards
Fg-index: towards verification-free query processing on graph databases (JC, YK, WN, AL), pp. 857–872.
WRLAWRLA-J-2004-MeseguerT07 #analysis #encryption #protocol #reachability #using #verification
Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols (JM, PT), pp. 123–160.
WRLAWRLA-2006-SasseM07 #algebra #hoare #java #logic #semantics #verification
Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics (RS, JM), pp. 29–46.
TACASTACAS-2007-AbdullaDHR #model checking #performance #transducer #verification
Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems) (PAA, GD, NBH, AR), pp. 721–736.
TACASTACAS-2007-CimattiRT #optimisation #verification
Syntactic Optimizations for PSL Verification (AC, MR, ST), pp. 505–518.
TACASTACAS-2007-FriasPM #alloy #analysis #specification #verification
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications (MFF, CLP, MMM), pp. 587–601.
TACASTACAS-2007-GheorghiuGP #composition #interface #verification
Refining Interface Alphabets for Compositional Verification (MG, DG, CSP), pp. 292–307.
TACASTACAS-2007-GoldmanK #composition #named #verification
MAVEN: Modular Aspect Verification (MG, SK), pp. 308–322.
SASSAS-2007-GallJ #automaton #infinity #representation #verification
Lattice Automata: A Representation for Languages on Infinite Alphabets, and Some Applications to Verification (TLG, BJ), pp. 52–68.
SASSAS-2007-MalkisPR #precise #thread #verification
Precise Thread-Modular Verification (AM, AP, AR), pp. 218–232.
SASSAS-2007-NandivadaPP #evaluation #framework #verification
A Framework for End-to-End Verification and Evaluation of Register Allocators (VKN, FMQP, JP), pp. 153–169.
SASSAS-2007-ShohamG #abstraction #composition #verification
Compositional Verification and 3-Valued Abstractions Join Forces (SS, OG), pp. 69–86.
LATALATA-2007-TorreNPP #state machine #verification
Verification of Succinct Hierarchical State Machines (SLT, MN, MP, GP), pp. 485–496.
IFMIFM-2007-BraghinSB #automation #mobile #policy #security #verification
Automated Verification of Security Policies in Mobile Code (CB, NS, KBA), pp. 37–53.
IFMIFM-2007-Bruckner #concurrent #realtime #slicing #specification #verification
Slicing Concurrent Real-Time System Specifications for Verification (IB), pp. 54–74.
IFMIFM-2007-FehnkerHM #modelling #network #protocol #verification
Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks (AF, LvH, AM), pp. 253–272.
IFMIFM-2007-HasanT #cumulative #probability #using #verification
Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function (OH, ST), pp. 333–352.
IFMIFM-2007-Metzler #specification #verification
Decomposing Integrated Specifications for Verification (BM), pp. 459–479.
IFMIFM-2007-OostdijkRTVW #encryption #learning #protocol #testing #verification
Integrating Verification, Testing, and Learning for Cryptographic Protocols (MO, VR, JT, RGdV, TACW), pp. 538–557.
IFMIFM-2007-PodorozhnyKPZ #alloy #multi #using #verification
Verification of Multi-agent Negotiations Using the Alloy Analyzer (RMP, SK, DEP, XZ), pp. 501–517.
IFMIFM-2007-PostK #linux #static analysis #verification
Integrated Static Analysis for Linux Device Driver Verification (HP, WK), pp. 518–537.
SEFMSEFM-2007-BeckertK #concurrent #deduction #logic #source code #verification
A Dynamic Logic for Deductive Verification of Concurrent Programs (BB, VK), pp. 141–150.
SEFMSEFM-2007-CansellGM #verification
Formal verification of tamper-evident storage for e-voting (DC, JPG, DM), pp. 329–338.
SEFMSEFM-2007-ColvinG #algorithm #scalability #stack #verification
A Scalable Lock-Free Stack Algorithm and its Verification (RC, LG), pp. 339–348.
SEFMSEFM-2007-CrockerC #automation #c #reasoning #source code #using #verification
Verification of C Programs Using Automated Reasoning (DC, JC), pp. 7–14.
SEFMSEFM-2007-MehraRSJ #relational #verification
Verification of Object Relational Maps (KKM, SKR, APS, SKJ), pp. 283–292.
SEFMSEFM-2007-SahaRC #modelling #protocol #using #verification
Modeling and Verification of TTCAN Startup Protocol Using Synchronous Calendar (IS, SR, KC), pp. 69–79.
AGTIVEAGTIVE-2007-BauerDTW #analysis #constraints #ocl #synthesis #verification
Verification and Synthesis of OCL Constraints Via Topology Analysis (JB, WD, TT, BW), pp. 361–376.
GT-VMTGT-VMT-2007-BisztrayH #csp #process #using #verification
Rule-Level Verification of Business Process Transformations using CSP (DB, RH).
GT-VMTGT-VMT-2007-RangelKE #approach #bisimulation #verification
Bisimulation Verification for the DPO Approach with Borrowed (GR, BK, HE).
HCIHCI-AS-2007-LinKTKT #design #development #process #verification #visual notation
Verification of Development of Scenarios Method and Visual Formats for Design Process (HL, MK, HT, HK, TT), pp. 1095–1101.
HCIHIMI-MTT-2007-SatoKF #concept #interface #precise #verification
Basic Experimental Verification of Grasping Information Interface Concept, Grasping Force Increases in Precise Periods (SS, MK, YF), pp. 180–188.
CAiSECAiSE-2007-MendlingA #formal method #verification
Formalization and Verification of EPCs with OR-Joins Based on State and Context (JM, WMPvdA), pp. 439–453.
ICEISICEIS-AIDSS-2007-Aalst #analysis #mining #process #roadmap #verification
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-DISI-2007-Aalst #analysis #mining #process #roadmap #verification
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-EIS-2007-Aalst #analysis #mining #process #roadmap #verification
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-EIS-2007-CombemaleGCTV #case study #process #towards #verification
Towards a Formal Verification of Process Model’s Properties SIMPLEPDL and TOCL Case Study (BC, PLG, XC, XT, FV), pp. 80–89.
ICEISICEIS-EIS-2007-SomeN #case study #consistency #requirements #verification
Use Case Based Requirements Verification — Verifying the Consistency between Use Cases and Assertions (SSS, DKN), pp. 190–195.
ICEISICEIS-HCI-2007-Aalst #analysis #mining #process #roadmap #verification
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-J-2007-CombemaleCGTV #approach #modelling #process #verification
A Property-Driven Approach to Formal Verification of Process Models (BC, XC, PLG, XT, FV), pp. 286–300.
ICEISICEIS-SAIC-2007-Aalst #analysis #mining #process #roadmap #verification
Trends in business process analysis — from verification to process mining (WMPvdA), pp. 5–9.
ICEISICEIS-SAIC-2007-BoukadiGMB #petri net #specification #using #verification #web #web service
Specification and Verification of Views over Composite Web Services Using High Level Petri-Nets (KB, CG, ZM, DB), pp. 107–112.
CIKMCIKM-2007-RoussinovT #online #semantics #verification
Semantic verification in an online fact seeking environment (DR, OT), pp. 71–78.
OOPSLAOOPSLA-2007-ChenR #framework #named #performance #runtime #verification
Mop: an efficient and generic runtime verification framework (FC, GR), pp. 569–588.
OOPSLAOOPSLA-2007-ShanerLN #composition #higher-order #source code #verification
Modular verification of higher-order methods with mandatory calls specified by model programs (SMS, GTL, DAN), pp. 351–368.
PADLPADL-2007-AlbertGHP #analysis #bytecode #java #logic programming #source code #using #verification
Verification of Java Bytecode Using Analysis and Transformation of Logic Programs (EA, MGZ, LH, GP), pp. 124–139.
POPLPOPL-2007-GulwaniJ #probability #verification
Program verification as probabilistic inference (SG, NJ), pp. 277–289.
POPLPOPL-2007-ParkinsonBO #composition #stack #verification
Modular verification of a non-blocking stack (MJP, RB, PWO), pp. 297–302.
SACSAC-2007-GooneratneTH #algorithm #graph #traversal #using #verification #web #web service
Verification of web service descriptions using graph-based traversal algorithms (NG, ZT, JH), pp. 1385–1392.
SACSAC-2007-Lamari #automation #generative #model transformation #testing #towards #verification
Towards an automated test generation for the verification of model transformations (ML), pp. 998–1005.
SACSAC-2007-Li #abstraction #parametricity #protocol #proving #verification
Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols (YL), pp. 1534–1535.
SACSAC-2007-MorimotoSGC #security #specification #verification
Formal verification of security specifications with common criteria (SM, SS, YG, JC), pp. 1506–1512.
SACSAC-2007-OliveiraAS #component #formal method #model checking #modelling #petri net #using #verification
Formal modelling and verification of a component model using coloured petri nets and model checking (EASO, HOdA, LDdS), pp. 1427–1431.
SACSAC-2007-PaliwalAB #distributed #using #verification #web #web service
Web service orchestration and verification using MSC and CP nets (AVP, NRA, CB), pp. 1693–1694.
SACSAC-2007-PloegerS #analysis #automation #documentation #verification
Analysis and verification of an automatic document feeder (BP, LJS), pp. 1499–1505.
SACSAC-2007-RaedtsPSWSB #automation #framework #verification
A software framework for automated verification (IR, MP, AS, JMEMvdW, LJS, MB), pp. 1031–1032.
SACSAC-2007-SantosBOJ #approach #documentation #forensics #verification
Off-line signature verification based on forensic questioned document examination approach (CRS, FB, LSO, EJRJ), pp. 637–638.
ESEC-FSEESEC-FSE-2007-AldrichBGLS #component #specification #verification
Specification and verification of component-based systems 2007 (JA, MB, DG, GTL, NS), pp. 609–610.
ESEC-FSEESEC-FSE-2007-Hanna #implementation #lightweight #named #network #protocol #security #verification
SLEDE: lightweight verification of sensor network security protocol implementations (YH), pp. 591–594.
ESEC-FSEESEC-FSE-2007-Kwiatkowska #modelling #tool support #verification
Quantitative verification: models techniques and tools (MZK), pp. 449–458.
ESEC-FSEESEC-FSE-2007-PradellaMP #symmetry #verification
The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties (MP, AM, PSP), pp. 312–320.
ICSEICSE-2007-BaresiGM #architecture #automation #on the #verification
On Accurate Automatic Verification of Publish-Subscribe Architectures (LB, CG, LM), pp. 199–208.
ICSEICSE-2007-GroceHJ #difference #random #testing #verification
Randomized Differential Testing as a Prelude to Formal Verification (AG, GJH, RJ), pp. 621–631.
COCVCOCV-2007-GallardoJM #analysis #data flow #on the fly #verification
On-the-Fly Data Flow Analysis Based on Verification Technology (MdMG, CJ, PM), pp. 33–48.
COCVCOCV-2007-Hamilton #source code #verification
Distilling Programs for Verification (GWH), pp. 17–32.
CADECADE-2007-GeBT #modulo theories #quantifier #satisfiability #using #verification
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories (YG, CB, CT), pp. 167–182.
CADECADE-2007-Leino #design #verification
Designing Verification Conditions for Software (KRML), p. 345.
CADECADE-2007-MurkLH #c #named #source code #verification
KeY-C: A Tool for Verification of C Programs (OM, DL, RH), pp. 385–390.
CADECADE-2007-VerchinineLP #automation #deduction #proving #verification
System for Automated Deduction (SAD): A Tool for Proof Verification (KV, AVL, AP), pp. 398–403.
CAVCAV-2007-AbdullaDR #infinity #process #verification
Parameterized Verification of Infinite-State Processes with Global Conditions (PAA, GD, AR), pp. 145–157.
CAVCAV-2007-BabicH #abstraction #verification
Structural Abstraction of Software Verification Conditions (DB, AJH), pp. 366–378.
CAVCAV-2007-BeyerHT #configuration management #convergence #model checking #program analysis #verification
Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis (DB, TAH, GT), pp. 504–518.
CAVCAV-2007-BruttomessoCFGHNPS #industrial #lazy evaluation #problem #smt #verification
A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems (RB, AC, AF, AG, ZH, AN, AP, RS), pp. 547–560.
CAVCAV-2007-ChakiSV #bound #verification
Verification Across Intellectual Property Boundaries (SC, CS, HV), pp. 82–94.
CAVCAV-2007-FilliatreM #deduction #framework #verification #why
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification (JCF, CM), pp. 173–177.
CAVCAV-2007-Franzle #hybrid #verification
Verification of Hybrid Systems (MF), p. 38.
CAVCAV-2007-GuptaMF #automation #composition #generative #verification
Automated Assumption Generation for Compositional Verification (AG, KLM, ZF), pp. 420–432.
CAVCAV-2007-LeavensKP #behaviour #composition #functional #java #ml #specification #tutorial #verification
A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java (GTL, JRK, EP), p. 37.
CAVCAV-2007-OuimetL #realtime #simulation #specification #tool support #verification
The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems (MO, KL), pp. 126–130.
CAVCAV-2007-PatinST #named #parallel #recursion #source code #thread #verification
Spade: Verification of Multithreaded Dynamic and Recursive Programs (GP, MS, TT), pp. 254–257.
CAVCAV-2007-PlakuKV #hybrid #verification
Hybrid Systems: From Verification to Falsification (EP, LEK, MYV), pp. 463–476.
CAVCAV-2007-Russinoff #approach #verification
A Mathematical Approach to RTL Verification (DMR), p. 2.
CAVCAV-2007-SinhaC #composition #lazy evaluation #learning #satisfiability #using #verification
SAT-Based Compositional Verification Using Lazy Learning (NS, EMC), pp. 39–54.
ICLPICLP-2007-MancarellaTT #abduction #logic programming #verification #web
Web Sites Verification: An Abductive Logic Programming Tool (PM, GT, FT), pp. 434–435.
MBTMBT-2007-OuimetL #automation #consistency #satisfiability #specification #state machine #using #verification
Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver (MO, KL), pp. 85–97.
RTARTA-2007-Leroy #compilation #optimisation #verification
Formal Verification of an Optimizing Compiler (XL), p. 1.
VMCAIVMCAI-2007-BouillaguetKWZR #data type #first-order #proving #theorem proving #using #verification
Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.
VMCAIVMCAI-2007-KlaedtkeRS #abstraction #hybrid #refinement #verification
Language-Based Abstraction Refinement for Hybrid System Verification (FK, SR, ZS), pp. 151–166.
VMCAIVMCAI-2007-Logozzo #abstract interpretation #analysis #composition #java #named #verification
Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes (FL), pp. 283–298.
VMCAIVMCAI-2007-Madhusudan #algorithm #learning #tutorial #verification
Learning Algorithms and Formal Verification (Invited Tutorial) (PM), p. 214.
VMCAIVMCAI-2007-NguyenDQC #automation #logic #verification
Automated Verification of Shape and Size Properties Via Separation Logic (HHN, CD, SQ, WNC), pp. 251–266.
VMCAIVMCAI-2007-RakamaricBH #data type #source code #verification
An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures (ZR, JDB, AJH), pp. 106–121.
VMCAIVMCAI-2007-Revesz #approach #constraints #database #verification
The Constraint Database Approach to Software Verification (PZR), pp. 329–345.
CBSECBSE-2006-AttieLPC #behaviour #component #design #explosion #verification
Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based Elevator Control System (PCA, DHL, AP, HC), pp. 33–49.
CBSECBSE-2006-XieB #component #product line #verification
Verification of Component-Based Software Application Families (FX, JCB), pp. 50–66.
ASEASE-2006-TateishiMOS #automation #verification
Automated Verification Tool for DHTML (TT, HM, KO, SS), pp. 363–364.
DACDAC-2006-BergeronFPMAS #testing #verification
Building a verification test plan: trading brute force for finesse (JB, HF, AP, RSM, CA, DS), pp. 805–806.
DACDAC-2006-BrierM #architecture #c #c++ #modelling #verification
Use of C/C++ models for architecture exploration and verification of DSPs (DB, RSM), pp. 79–84.
DACDAC-2006-DupenloupLM #abstraction #functional #verification
Transistor abstraction for the functional verification of FPGAs (GD, TL, RM), pp. 1069–1072.
DACDAC-2006-FengH #equivalence #verification
Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification (XF, AJH), pp. 1063–1068.
DACDAC-2006-Gluska #verification
Practical methods in coverage-oriented verification of the merom microprocessor (AG), pp. 332–337.
DACDAC-2006-GoraiBBTM #protocol #verification
Directed-simulation assisted formal verification of serial protocol and bridge (SG, SB, LB, PT, RSM), pp. 731–736.
DACDAC-2006-HosseiniPCUGB #design #question #standard #verification
Building a standard ESL design and verification methodology: is it just a dream? (AH, AP, HTC, PU, EFG, SB), pp. 370–371.
DACDAC-2006-NahirZEKR #generative #multi #testing #verification
Scheduling-based test-case generation for verification of multimedia SoCs (AN, AZ, RE, TK, NR), pp. 348–351.
DACDAC-2006-ShimizuGKOAMS #verification
Verification of the cell broadband engineTM processor (KS, SG, TK, TO, JA, LM, TS), pp. 338–343.
DACDAC-2006-Swan #modelling #transaction #verification
SystemC transaction level models and RTL verification (SS), pp. 90–92.
DATEDATE-2006-BalarinP #functional #generative #interface #specification #verification
Functional verification methodology based on formal interface specification and transactor generation (FB, RP), pp. 1013–1018.
DATEDATE-2006-BombieriFP #evaluation #on the #reuse #verification
On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL (NB, FF, GP), pp. 1007–1012.
DATEDATE-2006-FeyGD #verification
Avoiding false negatives in formal verification for protocol-driven blocks (GF, DG, RD), pp. 1225–1226.
DATEDATE-2006-HabibiTSLM #performance #using #verification
Efficient assertion based verification using TLM (AH, ST, AS, DL, OAM), pp. 106–111.
DATEDATE-2006-HassenT #on the #probability #term rewriting #verification
On the numerical verification of probabilistic rewriting systems (JBH, ST), pp. 1223–1224.
DATEDATE-2006-JerinicLHM #functional #metric #verification
New methods and coverage metrics for functional verification (VJ, JL, UH, DM), pp. 1025–1030.
DATEDATE-2006-KaneMS #pipes and filters #verification
Monolithic verification of deep pipelines with collapsed flushing (RK, PM, SKS), pp. 1234–1239.
DATEDATE-2006-KarlssonEP #design #petri net #representation #using #verification
Formal verification of systemc designs using a petri-net based representation (DK, PE, ZP), pp. 1228–1233.
DATEDATE-2006-MatulaM #algorithm #float #formal method #generative #performance #standard #traversal #verification
A formal model and efficient traversal algorithm for generating testbenches for verification of IEEE standard floating point division (DWM, LDM), pp. 1134–1138.
DATEDATE-2006-ShekharKE #equivalence #multi #verification
Equivalence verification of arithmetic datapaths with multiple word-length operands (NS, PK, FE), pp. 824–829.
DATEDATE-2006-ShyamB #hybrid #verification
Distance-guided hybrid verification with GUIDO (SS, VB), pp. 1211–1216.
DATEDATE-2006-WangYIG #embedded #image #verification
Disjunctive image computation for embedded software verification (CW, ZY, FI, AG), pp. 1205–1210.
DATEDATE-DF-2006-BonfiniCMP #verification
A mixed-signal verification kit for verification of analogue-digital circuits (GB, MC, RM, EP), pp. 88–93.
DATEDATE-DF-2006-Daglio #design #embedded #verification
A complete and fully qualified design flow for verification of mixed-signal SoC with embedded flash memories (PD), pp. 94–99.
DATEDATE-DF-2006-HuttonYSBCCP #synthesis #verification
A methodology for FPGA to structured-ASIC synthesis and verification (MH, RY, JS, GB, SC, KKC, HKP), pp. 64–69.
DATEDATE-DF-2006-ZarriCDMPRT #on the #protocol #verification
On the verification of automotive protocols (GZ, FC, FD, RM, MP, GR, CT), pp. 195–200.
DRRDRR-2006-ChenS #2d #recognition #verification
Combining one- and two-dimensional signal recognition approaches to off-line signature verification (SC, SNS).
PODSPODS-2006-DeutschSVZ #communication #data-driven #verification #web #web service
Verification of communicating data-driven web services (AD, LS, VV, DZ), pp. 90–99.
SIGMODSIGMOD-2006-DeutschSVZ #data-driven #interactive #specification #verification #web
A system for specification and verification of interactive, data-driven web applications (AD, LS, VV, DZ), pp. 772–774.
ESOPESOP-2006-LeinoM #verification
A Verification Methodology for Model Fields (KRML, PM), pp. 115–130.
TACASTACAS-2006-BrownP #protocol #verification
Easy Parameterized Verification of Biphase Mark and 8N1 Protocols (GMB, LP), pp. 58–72.
TACASTACAS-2006-CollavizzaR #constraints #programming #verification
Exploration of the Capabilities of Constraint Programming for Software Verification (HC, MR), pp. 182–196.
TACASTACAS-2006-DeshmukhEG #automation #data type #verification
Automatic Verification of Parameterized Data Structures (JVD, EAE, PG), pp. 27–41.
TACASTACAS-2006-HabermehlIV #source code #verification
Automata-Based Verification of Programs with Tree Updates (PH, RI, TV), pp. 350–364.
TACASTACAS-2006-HintonKNP #automation #named #probability #verification
PRISM: A Tool for Automatic Verification of Probabilistic Systems (AH, MZK, GN, DP), pp. 441–444.
TACASTACAS-2006-YangBR #verification #π-calculus
Parameterized Verification of π-Calculus Systems (PY, SB, CRR), pp. 42–57.
ICPCICPC-2006-RooverMGGD #approach #behaviour #documentation #lightweight #verification
An Approach to High-Level Behavioral Program Documentation Allowing Lightweight Verification (CDR, IM, KG, KG, TD), pp. 202–211.
PLDIPLDI-2006-FengSVXN #abstraction #assembly #composition #verification
Modular verification of assembly code with stack-based control abstractions (XF, ZS, AV, SX, ZN), pp. 401–414.
SASSAS-2006-LoginovRS #algorithm #automation #verification
Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm (AL, TWR, MS), pp. 261–279.
ICALPICALP-v1-2006-AulettaPPPV #verification
New Constructions of Mechanisms with Verification (VA, RDP, PP, GP, CV), pp. 596–607.
FMFM-2006-BlazyDL #c #compilation #verification
Formal Verification of a C Compiler Front-End (SB, ZD, XL), pp. 460–475.
FMFM-2006-BotaschanjanGHKST #distributed #towards #verification
Towards Modularized Verification of Distributed Time-Triggered Systems (JB, AG, AH, LK, MS, DT), pp. 163–178.
FMFM-2006-LiHR #automation #exception #safety #towards #verification
Towards Automatic Exception Safety Verification (XL, HJH, PR), pp. 396–411.
FMFM-2006-PnueliZ #model checking #runtime #verification
PSL Model Checking and Run-Time Verification Via Testers (AP, AZ), pp. 573–586.
FMFM-2006-Preoteasa #logic #pointer #recursion #using #verification
Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic (VP), pp. 508–523.
FMFM-2006-SchmittHBRM #guidelines #interactive #verification
Interactive Verification of Medical Guidelines (JS, AH, MB, WR, MM), pp. 32–47.
SEFMSEFM-2006-BeckertHS #deduction #design #object-oriented #verification
Integrating Object-Oriented Design and Deductive Verification of Software (BB, RH, PHS), p. 260.
SEFMSEFM-2006-Kapoor #formal method #modelling #pipes and filters #verification
Formal Modelling and Verification of an Asynchronous DLX Pipeline (HKK), pp. 118–127.
SEFMSEFM-2006-MarcheR #behaviour #java #transaction #verification
Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears (CM, NR), pp. 137–146.
SEFMSEFM-2006-RamsokulS #framework #modelling #named #protocol #verification #web service
ASEHA: A Framework for Modelling and Verification ofWeb Services Protocols (PR, AS), pp. 196–205.
SEFMSEFM-2006-Rushby #verification
Harnessing Disruptive Innovation in Formal Verification (JMR), pp. 21–30.
SFMSFM-2006-BombieriFP #design #hardware #simulation #verification
Hardware Design and Simulation for Verification (NB, FF, GP), pp. 1–29.
SFMSFM-2006-CabodiM #hardware #verification
BDD-Based Hardware Verification (GC, MM), pp. 78–107.
SFMSFM-2006-GuptaGW #hardware #satisfiability #verification
SAT-Based Verification Methods and Applications in Hardware Verification (AG, MKG, CW), pp. 108–143.
SFMSFM-2006-Harrison #float #proving #theorem proving #using #verification
Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.
AdaEuropeAdaEurope-2006-LiWQLYZZ #java #runtime #source code #specification #verification
Runtime Verification of Java Programs for Scenario-Based Specifications (XL, LW, XQ, BL, JY, JZ, GZ), pp. 94–105.
CAiSECAiSE-2006-WangR #modelling #verification #workflow
Dynamic Workflow Modeling and Verification (JW, DR), pp. 303–318.
EDOCEDOC-2006-BrennerAPMMS #component #re-engineering #testing #verification
Reducing Verification Effort in Component-Based Software Engineering through Built-In Testing (DB, CA, BP, RM, MM, DS), pp. 175–184.
ICPRICPR-v1-2006-DjiouaOP #interactive #recognition #verification
An interactive trajectory synthesizer to study outlier patterns in handwriting recognition and signature verification (MD, CO, RP), pp. 1124–1127.
ICPRICPR-v1-2006-LlanoVKM #representation #verification
An Illumination Insensitive Representation for Face Verification in the Frequency Domain (EGL, HMV, JK, KM), pp. 215–218.
ICPRICPR-v1-2006-WangCWG #invariant #recognition #verification
A Verification Method for Viewpoint Invariant Sign Language Recognition (QW, XC, CW, WG), pp. 456–459.
ICPRICPR-v1-2006-ZhouW06a #using #verification
Face Verification Using GaborWavelets and AdaBoost (MZ, HW), pp. 404–407.
ICPRICPR-v2-2006-ChenS #graph #verification
A New Off-line Signature Verification Method based on Graph (SC, SNS), pp. 869–872.
ICPRICPR-v2-2006-KhanKKA #dependence #online #verification
On-Line Signature Verification by Exploiting Inter-Feature Dependencies (MKK, MAK, MAUK, IA), pp. 796–799.
ICPRICPR-v2-2006-KimLKK #image #recognition #verification #video
Stroke Verification with Gray-level Image for Hangul Video Text Recognition (JK, SL, YK, JHK), pp. 1074–1077.
ICPRICPR-v2-2006-LiuHZ #independence #robust #verification
Robust Local Scoring Function for Text-Independent Speaker Verification (ML, TSH, ZZ), pp. 1146–1149.
ICPRICPR-v2-2006-QuanHXLL #analysis #online #verification
Spectrum Analysis Based onWindows with Variable Widths for Online Signature Verification (ZHQ, DSH, XLX, MRL, TML), pp. 1122–1125.
ICPRICPR-v2-2006-ShimshoniRS #classification #image #performance #verification
Efficient Search and Verification for Function Based Classification from Real Range Images (IS, ER, OS), pp. 1118–1121.
ICPRICPR-v2-2006-WeiGO #multi #verification
Fingerprint Verification Based on Multistage Minutiae Matching (HW, MG, ZO), pp. 1058–1061.
ICPRICPR-v4-2006-ArmandBM #verification
Off-line Signature Verification based on the Modified Direction Feature (SA, MB, VM), pp. 509–512.
ICPRICPR-v4-2006-ChaoTWC #framework #kernel #problem #testing #verification
A Kernel-based Discrimination Framework for Solving Hypothesis Testing Problems with Application to Speaker Verification (YHC, WHT, HMW, RCC), pp. 229–232.
ICPRICPR-v4-2006-LiuXYD #hybrid #verification
A New Hybrid GMM/SVM for Speaker Verification (ML, YX, ZY, BD), pp. 314–317.
ICPRICPR-v4-2006-NosratighodsAE #novel #set #using #verification
Speaker Verification Using A Novel Set of Dynamic Features (MN, EA, JE), pp. 266–269.
ICPRICPR-v4-2006-RyuKJ #adaptation #verification
Template Adaptation based Fingerprint Verification (CR, HK, AKJ), pp. 582–585.
ICPRICPR-v4-2006-ShuD #multi #verification
Multi-Biometrics Fusion for Identity Verification (CS, XD), pp. 493–496.
ICPRICPR-v4-2006-YangG06a #multi #using #verification
Multi-SNR GMMs-Based Noise-Robust Speaker Verification Using 1/fa Noises (LY, WG), pp. 241–244.
SEKESEKE-2006-CookeRW #verification
The Evolutionary Role of Variable Assignment and Its Impact on Program Verification (DEC, JNR, RGW), pp. 315–320.
SEKESEKE-2006-Sarna-StarostaSD #approach #concurrent #modelling #multi #thread
A Model-based Design-for-Verification Approach to Checking for Deadlock in Multi-threaded Applications (BSS, REKS, LKD), pp. 120–125.
GPCEGPCE-2006-LeavensABBCFHJMJSSS #roadmap #verification
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.
PPDPPPDP-2006-AlbertiGLCMM #abduction #framework #verification #web #web service
An abductive framework for a-priori verification of web services (MA, MG, EL, FC, PM, MM), pp. 39–50.
PADLPADL-2006-Wang #automation #model checking #verification
Automatic Verification of a Model Checker by Reflection (BYW), pp. 45–59.
SACSAC-2006-BurdyP #bytecode #java #specification #verification
Java bytecode specification and verification (LB, MP), pp. 1835–1839.
SACSAC-2006-DinechinLM #using #verification
Assisted verification of elementary functions using Gappa (FdD, CQL, GM), pp. 1318–1322.
SACSAC-2006-FilhoRR #coordination #exception #verification
Verification of coordinated exception handling (FCF, AR, CMFR), pp. 680–685.
SACSAC-2006-MalgouyresM #approach #consistency #formal method #metamodelling #uml #verification
A UML model consistency verification approach based on meta-modeling formalization (HM, GM), pp. 1804–1809.
SACSAC-2006-MorimotoSGC #security #specification #standard #verification
A security specification verification technique based on the international standard ISO/IEC 15408 (SM, SS, YG, JC), pp. 1802–1803.
SACSAC-2006-NasrBFI #automaton #specification #verification
Verification of a scheduler in B through a timed automata specification (ON, JPB, MF, MRI), pp. 1800–1801.
SACSAC-2006-Xing #strict
Enhancing program verifications by restricting object types (CCX), pp. 1816–1821.
ICSEICSE-2006-BeckerBGKS #adaptation #invariant #verification
Symbolic invariant verification for systems with dynamic structural adaptation (BB, DB, HG, FK, DS), pp. 72–81.
ICSEICSE-2006-FosterUMK #composition #modelling #named #verification #web #web service
LTSA-WS: a tool for model-based verification of web service compositions and choreography (HF, SU, JM, JK), pp. 771–774.
ICSEICSE-2006-TanAC #finite #verification
Managing space for finite-state verification (JT, GSA, LAC), pp. 152–161.
ICSEICSE-2006-Yin #approach #verification
The echo approach to formal verification (XY), pp. 981–984.
SPLCSPLC-2006-Scheidemann #distributed #embedded #evolution #optimisation #product line #verification
Optimizing the Selection of Representative Configurations in Verification of Evolving Product Lines of Distributed Embedded Systems (KDS), pp. 75–84.
AMOSTAMOST-J-2005-Robinson-MallettLMG06 #identification #model checking #using #verification
Extended state identification and verification using a model checker (CRM, PL, TM, UG), pp. 981–992.
CAVCAV-2006-BarnatBCMRS #distributed #named #verification
DiVinE — A Tool for Distributed Verification (JB, LB, IC, PM, PR, PS), pp. 278–281.
CAVCAV-2006-ColvinGLM #algorithm #concurrent #lazy evaluation #set #verification
Formal Verification of a Lazy Concurrent List-Based Set Algorithm (RC, LG, VL, MM), pp. 475–488.
CAVCAV-2006-GurfinkelWC #model checking #named #verification
Yasm: A Software Model-Checker for Verification and Refutation (AG, OW, MC), pp. 170–174.
CAVCAV-2006-Harel #aspect-oriented #game studies #source code #verification
Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs (DH), pp. 3–4.
CAVCAV-2006-KloseTWW #performance #sequence chart #verification
Check It Out: On the Efficient Formal Verification of Live Sequence Charts (JK, TT, BW, HW), pp. 219–233.
CAVCAV-2006-RoyZFH #consistency #memory management #performance #polynomial #verification
Fast and Generalized Polynomial Time Memory Consistency Verification (AR, SZ, CJF, JCH), pp. 503–516.
CAVCAV-2006-VardhanV #learning #named #verification
LEVER: A Tool for Learning Based Verification (AV, MV), pp. 471–474.
CSLCSL-2006-AtassiBT #logic #system f #verification
Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic (VA, PB, KT), pp. 150–166.
FATESFATES-RV-2006-LiD #algorithm #aspect-oriented #safety #testing #verification
Decompositional Algorithms for Safety Verification and Testing of Aspect-Oriented Systems (CL, ZD), pp. 100–114.
ICLPICLP-2006-Pientka #framework #logic #performance #verification
Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks (BP), pp. 3–10.
IJCARIJCAR-2006-Harrison #self #towards
Towards Self-verification of HOL Light (JH), pp. 177–191.
IJCARIJCAR-2006-SorgeMMC #automation #invariant #verification
Automatic Construction and Verification of Isotopy Invariants (VS, AM, RLM, SC), pp. 36–51.
ISSTAISSTA-2006-DennisCJ #composition #satisfiability #verification
Modular verification of code with SAT (GD, FSHC, DJ), pp. 109–120.
ISSTAISSTA-2006-FinkYDRG #alias #effectiveness #type system #verification
Effective typestate verification in the presence of aliasing (SJF, EY, ND, GR, EG), pp. 133–144.
LICSLICS-2006-Bryant #infinity #using #verification
Formal Verification of Infinite State Systems Using Boolean Methods (REB), pp. 3–4.
MBTMBT-2006-CallananGRSTZ #approach #monte carlo #runtime #verification
Runtime Verification for High-Confidence Systems: A Monte Carlo Approach (SC, RG, AR, SAS, MRT, EZ), pp. 41–52.
RTARTA-2006-Bryant #infinity #using #verification
Formal Verification of Infinite State Systems Using Boolean Methods (REB), pp. 1–3.
VMCAIVMCAI-2006-BozzelliTP #communication #recursion #state machine #verification
Verification of Well-Formed Communicating Recursive State Machines (LB, SLT, AP), pp. 412–426.
VMCAIVMCAI-2006-ClarkeTV #abstraction #verification
Environment Abstraction for Parameterized Verification (EMC, MT, HV), pp. 126–141.
ASEASE-2005-Betin-CanBLLT #concurrent #design #verification
Application of design for verification with concurrency controllers to air traffic control software (ABC, TB, ML, BL, ST), pp. 14–23.
ASEASE-2005-BlewittBS #automation #design pattern #java #verification
Automatic verification of design patterns in Java (AB, AB, IS), pp. 224–232.
ASEASE-2005-FriasGSB #analysis #performance #relational #specification #verification
A strategy for efficient verification of relational specifications, based on monotonicity analysis (MFF, RG, GS, LB), pp. 305–308.
DACDAC-2005-AbdollahiP #canonical #logic #performance #synthesis #verification
A new canonical form for fast boolean matching in logic synthesis and verification (AA, MP), pp. 379–384.
DACDAC-2005-AdirABPS #approach #architecture #testing #verification
A generic micro-architectural test plan approach for microprocessor verification (AA, HA, EB, OP, KS), pp. 769–774.
DACDAC-2005-AdirADLRVCCD #case study #named #parallel #verification
VLIW: a case study of parallelism verification (AA, YA, BD, YL, MR, MV, MAC, AC, GD), pp. 779–782.
DACDAC-2005-BacchiniMFBNMD #question #verification
Is methodology the highway out of verification hell? (FB, GM, HF, JB, MN, SM, LD), pp. 521–522.
DACDAC-2005-Chatterjee #design #process #verification
Streamline verification process with formal property verification to meet highly compressed design cycle (PC), pp. 674–677.
DACDAC-2005-EzerJ #configuration management #verification
Smart diagnostics for configurable processor verification (SE, SJ), pp. 789–794.
DACDAC-2005-Magee #development #matlab #realtime #testing #verification
Matlab extensions for the development, testing and verification of real-time DSP software (DPM), pp. 603–606.
DACDAC-2005-Rossi #design #formal method #question #scalability #verification
Can we really do without the support of formal methods in the verification of large designs? (UR), pp. 672–673.
DACDAC-2005-WolfsthalG #question #verification
Formal verification: is it real enough? (YW, RMG), pp. 670–671.
DATEDATE-2005-ChenLL #integration #layout #multi #verification
Integration, Verification and Layout of a Complex Multimedia SOC (CLC, JYL, YLL), pp. 1116–1117.
DATEDATE-2005-DasguptaY #architecture #modelling #verification
Modeling and Verification of Globally Asynchronous and Locally Synchronous Ring Architectures (SD, AY), pp. 568–569.
DATEDATE-2005-GanaiGA #embedded #memory management #modelling #performance #using #verification
Verification of Embedded Memory Systems using Efficient Memory Modeling (MKG, AG, PA), pp. 1096–1101.
DATEDATE-2005-GoossensDGPRR #design #network #performance #verification
A Design Flow for Application-Specific Networks on Chip with Guaranteed Performance to Accelerate SOC Design and Verification (KG, JD, OPG, SGP, AR, ER), pp. 1182–1187.
DATEDATE-2005-HabibiT #design #modelling #transaction #verification
Design for Verification of SystemC Transaction Level Models (AH, ST), pp. 560–565.
DATEDATE-2005-JacobiWPB #automation #multi #verification
Automatic Formal Verification of Fused-Multiply-Add FPUs (CJ, KW, VP, JB), pp. 1298–1303.
DATEDATE-2005-ManoliosS #modelling #performance #refinement #verification
Refinement Maps for Efficient Verification of Processor Models (PM, SKS), pp. 1304–1309.
DATEDATE-2005-ShashidharBCJ #algebra #equivalence #functional #source code #verification
Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code (KCS, MB, FC, GJ), pp. 1310–1315.
DRRDRR-2005-ChenD #feature model #verification
Sequence-matching-based feature extraction with applications to signature verification (YC, XD), pp. 76–83.
ICDARICDAR-2005-BulacuS #clustering #comparison #identification #verification
A Comparison of Clustering Methods for Writer Identification and Verification (MB, LS), pp. 1275–1279.
ICDARICDAR-2005-ChenS #verification
Use of Exterior Contours and Shape Features in Off-line Signature Verification (SC, SNS), pp. 1280–1284.
ICDARICDAR-2005-RichiardiKD #feature model #online #verification
Local and Global Feature Selection for On-line Signature Verification (JR, HK, AD), pp. 625–629.
ICDARICDAR-2005-RussellHBHM #using #verification
Dynamic Signature Verification Using Discriminative Training (GFR, JH, AB, AH, DM), pp. 1260–1264.
ICDARICDAR-2005-SrihariBBS #statistics #verification
A Statistical Model For Writer Verification (SNS, MJB, KB, VS), pp. 1105–1109.
ICDARICDAR-2005-WanW #modelling #online #statistics #verification
On-Line Signature Verification With Two-Stage Statistical Models (LW, BW), pp. 282–286.
ICDARICDAR-2005-YamazakiNTK #case study #online #verification
A Study on Vulnerability in On-line Writer Verification System (YY, AN, KT, NK), pp. 640–644.
WRLAWRLA-2004-CirsteaMR05 #java #programming #protocol #rule-based #verification
Rule-based Programming in Java For Protocol Verification (HC, PEM, AR), pp. 209–227.
WRLAWRLA-2004-MeseguerT05 #analysis #encryption #protocol #reachability #using #verification
Symbolic Reachability Analysis Using Narrowing and its Application to Verification of Cryptographic Protocols (JM, PT), pp. 153–182.
ESOPESOP-2005-ChanderEILN #bound #dynamic analysis #verification
Enforcing Resource Bounds via Static Verification of Dynamic Checks (AC, DE, NI, PL, GCN), pp. 311–325.
ESOPESOP-2005-LeeYY #analysis #automation #grammarware #pointer #source code #using #verification
Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis (OL, HY, KY), pp. 124–140.
FASEFASE-2005-Mostowski #formal method #java #logic #security #verification
Formalisation and Verification of Java Card Security Properties in Dynamic Logic (WM), pp. 357–371.
TACASTACAS-2005-BinghamH #empirical #infinity #performance #verification
Empirically Efficient Verification for a Class of Infinite-State Systems (JDB, AJH), pp. 77–92.
TACASTACAS-2005-EtessamiY #algorithm #probability #recursion #state machine #verification
Algorithmic Verification of Recursive Probabilistic State Machines (KE, MY), pp. 253–270.
TACASTACAS-2005-GenestKMP #verification
Snapshot Verification (BG, DK, AM, DP), pp. 510–525.
TACASTACAS-2005-SchwoonE #algorithm #on the fly #verification
A Note on On-the-Fly Verification Algorithms (SS, JE), pp. 174–190.
SCAMSCAM-2005-ZhangBCD #implementation #using #verification
Implementation and Verification of Implicit-Invocation Systems Using Source Transformation (HZ, JSB, JRC, JD), pp. 87–96.
SASSAS-2005-ChinNQR #memory management #object-oriented #source code #verification
Memory Usage Verification for OO Programs (WNC, HHN, SQ, MCR), pp. 70–86.
ICALPICALP-2005-DelzannoG #composition #constraints #process #theorem proving #verification
Compositional Verification of Asynchronous Processes via Constraint Solving (GD, MG), pp. 1239–1250.
ICALPICALP-2005-LiDIY #problem #verification
Signaling P Systems and Verification Problems (CL, ZD, OHI, HCY), pp. 1462–1473.
FMFM-2005-AndronickCP #embedded #security #smarttech #source code #verification
Formal Verification of Security Properties of Smart Card Embedded Source Code (JA, BC, CPM), pp. 302–317.
FMFM-2005-BasinKTW #architecture #verification
Verification of a Signature Architecture with HOL-Z (DAB, HK, KT, BW), pp. 269–285.
FMFM-2005-ButlerL #csp #specification #verification
Combining CSP and B for Specification and Property Verification (MJB, ML), pp. 221–236.
FMFM-2005-Harrison #float #verification
Floating-Point Verification (JH), pp. 529–532.
FMFM-2005-LeinoM #composition #invariant #verification
Modular Verification of Static Class Invariants (KRML, PM), pp. 26–42.
FMFM-2005-RusuMJ #automation #consistency #safety #testing #validation #verification
Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems (VR, HM, TJ), pp. 189–204.
IFMIFM-2005-ChakiCGOSTV #specification #verification
State/Event Software Verification for Branching-Time Specifications (SC, EMC, OG, JO, NS, TT, HV), pp. 53–69.
IFMIFM-2005-Lang #composition #flexibility #on the fly #partial order #verification
Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods (FL), pp. 70–88.
IFMIFM-2005-SchneiderTE #component #csp #named #verification
Chunks: Component Verification in CSP||B (SAS, HT, NE), pp. 89–108.
SEFMSEFM-2005-BlechGG #higher-order #verification
Formal Verification of Dead Code Elimination in Isabelle/HOL (JOB, LG, SG), pp. 200–209.
SEFMSEFM-2005-GrandySR #java #kernel #object-oriented #verification
Object Oriented Verification Kernels for Secure Java Applications (HG, KS, WR), pp. 170–179.
SEFMSEFM-2005-HubertM #algorithm #c #case study #source code #verification
A case study of C source code verification: the Schorr-Waite algorithm (TH, CM), pp. 190–199.
SEFMSEFM-2005-LeinenbachPP #code generation #compilation #implementation #towards #verification
Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes (DL, WJP, EP), pp. 2–12.
SEFMSEFM-2005-NivelleP #verification
Verification of an Off-Line Checker for Priority Queues (HdN, RP), pp. 210–219.
SEFMSEFM-2005-PrasetyaAVL #composition #generative #verification
Building Verification Condition Generators by Compositional Extensions (ISWBP, AA, TEJV, AvL), pp. 220–230.
SEFMSEFM-2005-SadaniSC #framework #petri net #verification
From RT-LOTOS to Time Petri Nets New Foundations for a Verification Platform (TS, PdSS, JPC), pp. 250–260.
SEFMSEFM-2005-Trakhtenbrot #debugging #testing #verification
Use of Verification for Testing and Debugging of Complex Reactive Systems (MBT), pp. 13–22.
SEFMSEFM-2005-WilsonMC #approach #configuration management #flexibility #policy #verification
Omnibus Verification Policies: A flexible, configurable approach to assertion-based software verification (TW, SM, RGC), pp. 150–159.
ICFPICFP-2005-FengS #assembly #composition #concurrent #termination #thread #verification
Modular verification of concurrent assembly code with dynamic thread creation and termination (XF, ZS), pp. 254–267.
AdaEuropeAdaEurope-2005-EvangelistaKPPR #verification
Dynamic Tasks Verification with Quasar (SE, CK, CP, JFPP, PR), pp. 91–104.
CAiSECAiSE-2005-DongenAV #petri net #reduction #using #verification
Verification of EPCs: Using Reduction Rules and Petri Nets (BFvD, WMPvdA, HMWV), pp. 372–386.
CIKMCIKM-2005-RoussinovFN #semantics #verification
Semantic verification for fact seeking engines (DR, WF, FADN), pp. 323–324.
SEKESEKE-2005-BrandaoSL #design #knowledge-based #multi #reasoning #using #verification
Multi-Agent System Design Verification Using Knowledge-based Reasoning (AB, VTdS, CJPdL), pp. 602–607.
SEKESEKE-2005-Chang05a #database #peer-to-peer #verification
Peer-To-Peer Trading Databases Verification and Rectification (PC), pp. 772–776.
SEKESEKE-2005-HsiungL #modelling #safety #verification
Model-based Verification of Safety-Critical Systems (PAH, YHL), pp. 596–601.
SEKESEKE-2005-HsuehCK #design pattern #modelling #object-oriented #quality #verification
Verification of Design Patterns with Object-Oriented Quality Models (NLH, PHC, JYK), pp. 193–198.
SEKESEKE-2005-OgataF #approach #liveness #proving #verification
Proof Score Approach to Verification of Liveness Properties (KO, KF), pp. 608–613.
SEKESEKE-2005-SongPCZ #specification #transaction #uml #verification
Formal Verification of Transactional Systems Based on UML Specifications (MAJS, AMP, SVAC, LEZ), pp. 199–204.
ECOOPECOOP-2005-RodriguezDFHLR #composition #concurrent #ml #multi #source code #specification #thread #verification
Extending JML for Modular Specification and Verification of Multi-threaded Programs (ER, MBD, CF, JH, GTL, R), pp. 551–576.
LOPSTRLOPSTR-2005-PettorossiPS #array #protocol #using #verification
Transformational Verification of Parameterized Protocols Using Array Formulas (AP, MP, VS), pp. 23–43.
RERE-2005-ToyamaO #rule-based #verification
Rule-based Verification of Scenarios with Pre-conditions and Post-conditions (TT, AO), pp. 319–328.
SACSAC-2005-RekhisB #automation #forensics #verification
A formal logic-based language and an automated verification tool for computer forensic investigation (SR, NB), pp. 287–291.
SACSAC-2005-TruongS #behaviour #modelling #uml #using #verification
Verification of behavioural elements of UML models using B (NTT, JS), pp. 1546–1552.
SACSAC-2005-YangEY05a #framework #modelling #verification
Mediation framework modeling and verification by SAM (LY, RKE, HY), pp. 1567–1568.
ESEC-FSEESEC-FSE-2005-Sherriff #fault #validation #verification
Utilizing verification and validation certificates to estimate software defect density (MS), pp. 381–384.
ICSEICSE-2005-BeekMLGFS #automation #case study #protocol #verification
A case study on the automated verification of groupware protocols (MHtB, MM, DL, SG, AF, MS), pp. 596–603.
ICSEICSE-2005-FislerKMT #impact analysis #policy #verification
Verification and change-impact analysis of access-control policies (KF, SK, LAM, MCT), pp. 196–205.
SPLCSPLC-2005-KishiNK #design #development #product line #verification
Design Verification for Product Line Development (TK, NN, TK), pp. 150–161.
CCCC-2005-ShashidharBCJ #equivalence #program transformation #source code #verification
Verification of Source Code Transformations by Program Equivalence Checking (KCS, MB, FC, GJ), pp. 221–236.
PPoPPPPoPP-2005-SiegelA #modelling #source code #verification
Modeling wildcard-free MPI programs for verification (SFS, GSA), pp. 95–106.
AMOSTAMOST-2005-LiN #image #modelling #testing #validation #verification
Modeling for image processing system validation, verification and testing (XL, RN).
CADECADE-2005-BryantS #verification
Decision Procedures Customized for Formal Verification (REB, SAS), pp. 255–259.
CADECADE-2005-Lev-AmiIRSSY #data type #first-order #linked data #logic #open data #reachability #simulation #using #verification
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures (TLA, NI, TWR, SS, SS, GY), pp. 99–115.
CAVCAV-2005-0002G #modelling #probability #protocol #verification
Improved Probabilistic Models for 802.11 Protocol Verification (AR, KG), pp. 239–252.
CAVCAV-2005-AlurMN #composition #learning #verification
Symbolic Compositional Verification by Learning Assumptions (RA, PM, WN), pp. 548–562.
CAVCAV-2005-AronsEFMMSSTVZ #verification
Formal Verification of Backward Compatibility of Microcode (TA, EE, LF, SMH, MM, JS, ES, AT, MYV, LDZ), pp. 185–198.
CAVCAV-2005-BenediktBFV #optimisation #verification
Verification of Tree Updates for Optimization (MB, AB, SF, AV), pp. 379–393.
CAVCAV-2005-CookKS #named #proving #theorem proving #verification
Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.
CAVCAV-2005-IvancicYGGSA #framework #named #verification
F-Soft: Software Verification Platform (FI, ZY, MKG, AG, IS, PA), pp. 301–306.
CAVCAV-2005-Kaivola #component #induction #invariant #simulation #verification
Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants (RK), pp. 170–184.
CAVCAV-2005-NeculaG #algorithm #program analysis #random #verification
Randomized Algorithms for Program Analysis and Verification (GCN, SG), p. 1.
CAVCAV-2005-PastorPS #concurrent #named #verification
TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems (EP, MAP, MS), pp. 424–428.
CAVCAV-2005-Younes #black box #probability #verification
Probabilistic Verification for “Black-Box” Systems (HLSY), pp. 253–265.
CSLCSL-2005-Slissenko #algorithm #logic #verification
Verification in Predicate Logic with Time: Algorithmic Questions (AS), pp. 3–17.
ICLPICLP-2005-Chesani #formal method #interactive #protocol #verification
Formalization and Verification of Interaction Protocols (FC), pp. 437–438.
LICSLICS-2005-BlanchetAF #automation #protocol #security #verification
Automated Verification of Selected Equivalences for Security Protocols (BB, MA, CF), pp. 331–340.
ICTSSTestCom-2005-Maibaum #testing #validation #verification
The Epistemology of Validation and Verification Testing (TSEM), pp. 1–8.
VMCAIVMCAI-2005-Hymans #abstract interpretation #fault #verification
Verification of an Error Correcting Code by Abstract Interpretation (CH), pp. 330–345.
VMCAIVMCAI-2005-Siegel #performance #source code #verification
Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives (SFS), pp. 413–429.
ASEASE-2004-BlundellFKH #interface #product line #verification
Parameterized Interfaces for Open System Verification of Product Lines (CB, KF, SK, PVH), pp. 258–267.
ASEASE-2004-Haydar #analysis #automation #framework #verification
Formal Framework for Automated Analysis and Verification of Web-Based Applications (MH), pp. 410–413.
ASEASE-2004-Xie #approach #component #hybrid #verification
Decompositional Verification of Component-based Systems — A Hybrid Approach (GX), pp. 414–417.
DACDAC-2004-AndrausS #abstraction #automation #modelling #verification
Automatic abstraction and verification of verilog models (ZSA, KAS), pp. 218–223.
DACDAC-2004-BacchiniDBBNIY #named #verification #what
Verification: what works and what doesn’t (FB, RFD, BB, KB, KN, MI, EY), p. 274.
DACDAC-2004-BehmLLRV #experience #generative #industrial #testing #verification
Industrial experience with test generation languages for processor verification (MLB, JML, YL, MR, MV), pp. 36–40.
DACDAC-2004-FineUZ #functional #probability #verification
Probabilistic regression suites for functional verification (SF, SU, AZ), pp. 49–54.
DACDAC-2004-NakamuraHKYY #c #c++ #communication #hardware #performance #using
A fast hardware/software co-verification method for system-on-a-chip by using a C/C++ simulator and FPGA emulator with shared register communication (YN, KH, IK, KY, TY), pp. 299–304.
DATEDATE-DF-2004-BaileyMBLA #design #verification
Improving Design and Verification Productivity with VHDL-200x (SB, EM, JB, JL, PJA), pp. 332–335.
DATEDATE-DF-2004-SchmittR #design #low cost #prototype #using #verification
Verification of a Microcontroller IP Core for System-on-a-Chip Designs Using Low-Cost Prototyping Environments (SS, WR), pp. 96–101.
DATEDATE-v1-2004-BasuDDCMF #architecture #design #question #verification
Formal Verification Coverage: Are the RTL-Properties Covering the Design’s Architectural Intent? (PB, SD, PD, PPC, CRM, LF), pp. 668–669.
DATEDATE-v1-2004-DSilvaRS #architecture #automaton #communication #framework #modelling #protocol #verification
Synchronous Protocol Automata: A Framework for Modelling and Verification of SoC Communication Architectures (VD, SR, AS), pp. 390–395.
DATEDATE-v1-2004-ManoliosS #automation #liveness #modelling #safety #using #verification #web
Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements (PM, SKS), pp. 168–175.
DATEDATE-v1-2004-PostVRS #verification
A SystemC-Based Verification Methodology for Complex Wireless Software IP (GP, PKV, TR, DRS), pp. 544–551.
DATEDATE-v1-2004-RaudvereSSJ #abstraction #polynomial #verification
Polynomial Abstraction for Verification of Sequentially Implemented Combinational Circuits (TR, AKS, IS, AJ), pp. 690–691.
DATEDATE-v1-2004-Velev #performance #verification
Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors (MNV), pp. 266–271.
DATEDATE-v1-2004-WinkelmannTSF #low cost #verification
Cost-Efficient Block Verification for a UMTS Up-Link Chip-Rate Coprocessor (KW, HJT, DS, GF), pp. 162–167.
DATEDATE-v2-2004-Singh #co-evolution #design
A Demonstration of Co-Design and Co-Verification in a Synchronous Language (SS), pp. 1394–1395.
DATEDATE-2005-BorgattiCRLMFP04 #configuration management #design #multi #verification
An Integrated Design and Verification Methodology for Reconfigurable Multimedia Systems (MB, AC, UR, JLL, IM, FF, GP), pp. 266–271.
DATEDATE-2005-FalconeriNR04 #modelling #reuse #verification
Common Reusable Verification Environment for BCA and RTL Models (GF, WN, NR), pp. 272–277.
DATEDATE-2005-HabibiAMT04 #design #interface #on the #verification
On the Design and Verification Methodology of the Look-Aside Interface (AH, AIA, OAM, ST), pp. 290–295.
DATEDATE-2005-MacBethHG04a #assembly #verification
An Assembler Driven Verification Methodology (ADVM) (JSM, DH, KG), pp. 278–283.
DATEDATE-2005-UmezawaS04 #verification
A Formal Verification Methodology for Checking Data Integrity (YU, TS), pp. 284–289.
PODSPODS-2004-DeutschSV #data-driven #specification #verification #web #web service
Specification and Verification of Data-driven Web Services (AD, LS, VV), pp. 71–82.
ITiCSEITiCSE-2004-Tanaka-IshiiKT #feedback #named #programming #verification
EMMA: a web-based report system for programming course--automated verification and enhanced feedback (KTI, KK, MT), p. 278.
FASEFASE-2004-BartheD #bytecode #framework #verification
A Tool-Assisted Framework for Certified Bytecode Verification (GB, GD), pp. 99–113.
FASEFASE-2004-ChildsGRDDHJSS #analysis #component #development #ide #named #synthesis #verification
Cadena: An Integrated Development Environment for Analysis, Synthesis, and Verification of Component-Based Systems (AC, JG, VPR, XD, MBD, JH, GJ, PS, GS), pp. 160–164.
TACASTACAS-2004-AbramskyGMO #composition #game studies #modelling #semantics #verification
Applying Game Semantics to Compositional Software Modeling and Verification (SA, DRG, ASM, CHLO), pp. 421–435.
TACASTACAS-2004-BeauquierCP #automation #first-order #logic #parametricity #protocol #state machine #verification
Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic (DB, TC, EP), pp. 372–387.
TACASTACAS-2004-DelzannoG #automation #encryption #protocol #verification
Automatic Verification of Time Sensitive Cryptographic Protocols (GD, PG), pp. 342–356.
TACASTACAS-2004-DiethersH #design #named #object-oriented #using #verification
Vooduu: Verification of Object-Oriented Designs Using UPPAAL (KD, MH), pp. 139–143.
TACASTACAS-2004-GeldenhuysV #algorithm #ltl #on the fly #performance #verification
Tarjan’s Algorithm Makes On-the-Fly LTL Verification More Efficient (JG, AV), pp. 205–219.
TACASTACAS-2004-LindseyP #verification
Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder (AEL, CP), pp. 357–371.
TACASTACAS-2004-VirtanenHVNE #verification
Tampere Verification Tool (HV, HH, AV, JN, TE), pp. 153–157.
PEPMPEPM-2004-BeyerCHJM #query #verification
Invited talk: the blast query language for software verification (DB, AC, TAH, RJ, RM), pp. 201–202.
PEPMPEPM-2004-PopeeaC #correctness #protocol #proving #type system #verification
A type system for resource protocol verification and its correctness proof (CP, WNC), pp. 135–146.
SASSAS-2004-BeyerCHJM #query #verification
The Blast Query Language for Software Verification. (DB, AC, TAH, RJ, RM), pp. 2–18.
CIAACIAA-2004-DaleyM #complexity #verification
Viral Gene Compression: Complexity and Verification (MD, IM), pp. 102–112.
ICALPICALP-2004-AulettaPPP #power of #verification
The Power of Verification for One-Parameter Agents (VA, RDP, PP, GP), pp. 171–182.
IFMIFM-2004-BeckertS #data type #integer #refinement #verification
Software Verification with Integrated Data Type Refinement for Integer Arithmetic (BB, SS), pp. 207–226.
IFMIFM-2004-BoultonGHKM #design #verification
Design Verification for Control Engineering (RJB, HG, RH, TK, UM), pp. 21–35.
IFMIFM-2004-CiobanuL #concurrent #specification #verification
Specification and Verification of Synchronizing Concurrent Objects (GC, DL), pp. 307–327.
IFMIFM-2004-LanoCA #modelling #object-oriented #uml #verification
UML to B: Formal Verification of Object-Oriented Models (KL, DC, KA), pp. 187–206.
SEFMSEFM-2004-BeckertK #deduction #proving #reuse #verification
Proof Reuse for Deductive Program Verification (BB, VK), pp. 77–86.
SEFMSEFM-2004-HeJ #transaction #verification
Verification of the WAP Transaction Layer (YTH, RJ), pp. 366–375.
SEFMSEFM-2004-KazhamiakinPR #case study #requirements #using #verification #web #web service
Formal Verification of Requirements using SPIN: A Case Study on Web Services (RK, MP, MR), pp. 406–415.
SEFMSEFM-2004-Roy #finite #infinity #using #verification
Symbolic Verification of Infinite Systems using a Finite Union of DFAs (SR), pp. 56–66.
SEFMSEFM-2004-SchinzTMW #uml #verification
The Rhapsody UML Verification Environment (IS, TT, CM, BW), pp. 174–183.
SEFMSEFM-2004-SchuleS #comparison #infinity #model checking #verification
Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems (TS, KS), pp. 67–76.
ICFPICFP-2004-YuS #assembly #concurrent #safety #verification
Verification of safety properties for concurrent assembly code (DY, ZS), pp. 175–188.
EDOCEDOC-2004-WoodmanPSW #specification #verification #web #web service
Notations for the Specification and Verification of Composite Web Services (SJW, DJP, SKS, SMW), pp. 35–46.
ICEISICEIS-v1-2004-Augusto #model checking #theorem proving #verification
Model Checking and Theorem Proving-Based Verification of EIS (JCA), p. XXXIII-XXXIV.
ICEISICEIS-v3-2004-AliBG #dependence #diagrams #uml #verification
UML Model Verification Through Diagram Dependency Relationships (MA, HBA, FG), pp. 184–191.
ICEISICEIS-v3-2004-SchuetzelhoferG #domain model #modelling #specification #verification #xml
Formal Specification and Verification of XML-Based Business Domain Models (WS, KMG), pp. 209–216.
ICMLICML-2004-KoppelS #classification #problem #verification
Authorship verification as a one-class classification problem (MK, JS).
ICPRICPR-v1-2004-BourlaiMK #architecture #smarttech #using #verification
Face Verification System Architecture Using Smart Cards (TB, KM, JK), pp. 793–796.
ICPRICPR-v1-2004-KongZ #verification
Competitive Coding Scheme for Palmprint Verification (AWKK, DZ), pp. 520–523.
ICPRICPR-v2-2004-BaiH #approach #documentation #image
A Goal-Oriented Verification-Based Approach for Target Text Line Extraction from a Document Image Captured by a Pen Scanner (ZLB, QH), pp. 574–577.
ICPRICPR-v2-2004-KimBSCCKC #image #using #verification
Scene Text Extraction in Natural Scene Images using Hierarchical Feature Combining and Verification (KCK, HRB, YJS, YWC, SYC, KKK, YC), pp. 679–682.
ICPRICPR-v3-2004-NaderiMC #algorithm #image #optimisation #using #verification
1D-HMM for Face Verification: Model Optimization Using Improved Algorithm and Intelligent Selection of Training Images (SN, MSM, NMC), pp. 330–333.
ICPRICPR-v4-2004-FanL #image #using #verification
The Using of Thermal Images of Palm-dorsa Vein-patterns for Biometric Verification (KCF, CLL), pp. 450–453.
ICPRICPR-v4-2004-LiuSCH #clustering #personalisation #using #verification
Personalized Face Verification System Using Owner-Specific Cluster-Dependent LDA-Subspace (HCL, CHS, YHC, YPH), pp. 344–347.
SEKESEKE-2004-ChenS #interactive #protocol #specification #verification
Specification and Verification of Agent Interaction Protocols (BC, SS), pp. 300–305.
SIGIRSIGIR-2004-Martin #natural language #reliability #verification #web
Reliability and verification of natural language text on the world wide web (abstract only) (MJM), p. 603.
UMLUML-2004-AronsHKPZ #deduction #modelling #uml #verification
Deductive Verification of UML Models in TLPVS (TA, JH, HK, AP, MvdZ), pp. 335–349.
UMLUML-2004-JurjensS #automation #modelling #requirements #security #verification
Automated Verification of UMLsec Models for Security Requirements (JJ, PS), pp. 365–379.
OOPSLAOOPSLA-2004-Fong #verification #virtual machine
Pluggable verification modules: an extensible protection mechanism for the JVM (PWLF), pp. 404–418.
LOPSTRLOPSTR-2004-KulkarniBE #automation #fault tolerance #source code #synthesis #verification
Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs (SSK, BB, AE), pp. 36–52.
LOPSTRPDCL-2004-RoychoudhuryR #automation #concurrent #verification
Unfold/Fold Transformations for Automated Verification of Parameterized Concurrent Systems (AR, CRR), pp. 261–290.
PPDPPPDP-2004-BeyerCHJM #query #verification
Invited talk: the blast query language for software verification (DB, AC, TAH, RJ, RM), pp. 1–2.
PPDPPPDP-2004-ClevaLL #approach #functional #logic programming #source code #verification
A logic programming approach to the verification of functional-logic programs (JMC, JL, FJLF), pp. 9–19.
SACSAC-2004-AlbertiDTGLM #interactive #protocol #specification #verification
Specification and verification of agent interaction protocols in a logic-based system (MA, DD, PT, MG, EL, PM), pp. 72–78.
SACSAC-2004-BarbutiC #bytecode #java #verification
Java bytecode verification on Java cards (RB, SC), pp. 431–438.
SACSAC-2004-DiazCRP #automation #protocol #verification
Automatic verification of the TLS handshake protocol (GD, FC, VVR, FLP), pp. 789–794.
SACSAC-2004-TangMC #embedded #fixpoint #implementation #mobile #performance #using #verification
Efficient implementation of fingerprint verification for mobile embedded systems using fixed-point arithmetic (TYT, YSM, KCC), pp. 821–825.
FSEFSE-2004-GieseBSO #component #composition #configuration management #design #verification
Modular design and verification of component-based mechatronic systems with online-reconfiguration (HG, SB, WS, OO), pp. 179–188.
ICSEICSE-2004-CaporuscioIP #architecture #composition #middleware #verification
Compositional Verification of Middleware-Based Software Architecture Descriptions (MC, PI, PP), pp. 221–230.
ICSEICSE-2004-GiannakopoulouPC #source code #verification
Assume-Guarantee Verification of Source Code with Design-Level Assumptions (DG, CSP, JMC), pp. 211–220.
SPLCSPLC-2004-FantechiGLN #case study #product line #verification
A Methodology for the Derivation and Verification of Use Cases for Product Lines (AF, SG, GL, EN), pp. 255–265.
CAVCAV-2004-Arons #algorithm #execution #verification
Verification of an Advanced mips-Type Out-of-Order Execution Algorithm (TA), pp. 414–426.
CAVCAV-2004-BinghamCHQZ #automation #bound #consistency #verification
Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values (JDB, AC, AJH, SQ, ZZ), pp. 427–439.
CAVCAV-2004-ChangBD #design #interface #refinement #using #verification
Using Interface Refinement to Integrate Formal Verification into the Design Cycle (JC, SB, DLD), pp. 122–134.
CAVCAV-2004-GopalakrishnanYS #execution #memory management #order #performance #verification
QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings (GG, YY, HS), pp. 401–413.
CAVCAV-2004-Hunt #verification
Mechanical Mathematical Methods for Microprocessor Verification (WAHJ), pp. 523–533.
CAVCAV-2004-ImmermanRRSY #simulation #verification
Verification via Structure Simulation (NI, AMR, TWR, SS, GY), pp. 281–294.
CAVCAV-2004-JiangB #dependence #functional #reduction #verification
Functional Dependency for Verification Reduction (JHRJ, RKB), pp. 268–280.
CAVCAV-2004-LahiriB #bound #verification
Indexed Predicate Discovery for Unbounded System Verification (SKL, REB), pp. 135–147.
CAVCAV-2004-RameshSDCV #modelling #tool support #verification
A Toolset for Modelling and Verification of GALS Systems (SR, SS, VD, NC, BV), pp. 506–509.
CAVCAV-2004-RayH #deduction #first-order #pipes and filters #quantifier #using #verification
Deductive Verification of Pipelined Machines Using First-Order Quantification (SR, WAHJ), pp. 31–43.
CSLCSL-2004-AmadioCDJ #bound #bytecode #functional #verification
A Functional Scenario for Bytecode Verification of Resource Bounds (RMA, SCG, SDZ, LJ), pp. 265–279.
CSLCSL-2004-Weber #logic #towards #verification
Towards Mechanized Program Verification with Separation Logic (TW), pp. 250–264.
ICLPICLP-2004-RamirezM #constraints #distributed #java #source code #verification
Constraint-Based Synchronization and Verification of Distributed Java Programs (RR, JM), pp. 473–474.
RTARTA-2004-Takai #abstract interpretation #term rewriting #using #verification
A Verification Technique Using Term Rewriting Systems and Abstract Interpretation (TT), pp. 119–133.
ICTSSTestCom-2004-RusuMTJJ #safety #testing #verification
From Safety Verification to Safety Testing (VR, HM, VT, TJ, BJ), pp. 160–176.
VMCAIVMCAI-2004-BarringerGHS #rule-based #runtime #verification
Rule-Based Runtime Verification (HB, AG, KH, KS), pp. 44–57.
ASEASE-2003-BunusF #automation #behaviour #fault #locality #modelling #physics #simulation #verification
Semi-Automatic Fault Localization and Behavior Verification for Physical System Simulation Models (PB, PF), pp. 253–258.
ASEASE-2003-FosterUMK #composition #modelling #verification #web #web service
Model-based Verification of Web Service Compositions (HF, SU, JM, JK), pp. 152–163.
DACDAC-2003-FineZ #functional #generative #network #testing #using #verification
Coverage directed test generation for functional verification using bayesian networks (SF, AZ), pp. 286–291.
DACDAC-2003-Gluska #verification
Coverage-oriented verification of banias (AG), pp. 280–285.
DACDAC-2003-GuptaRSBBFPOS #verification
Formal verification — prove it or pitch it (RKG, SR, SKS, BB, DKB, MF, CP, JO, FS), pp. 710–711.
DACDAC-2003-HuangC #embedded #framework #using #verification
Using embedded infrastructure IP for SOC post-silicon verification (YH, WTC), pp. 674–677.
DACDAC-2003-KouroussisN #grid #independence #power management #verification
A static pattern-independent technique for power grid voltage integrity verification (DK, FNN), pp. 99–104.
DACDAC-2003-MathysC #integration #verification
Verification strategy for integration 3G baseband SoC (YM, AC), pp. 7–10.
DACDAC-2003-Schubert #verification
High level formal verification of next-generation microprocessors (TS), pp. 1–6.
DACDAC-2003-YuanAAP #constraints #functional #modelling #synthesis #verification
Constraint synthesis for environment modeling in functional verification (JY, KA, AA, CP), pp. 296–299.
DATEDATE-2003-AndritsopoulosCDKMPTPR #case study #verification
Verification of a Complex SoC: The PRO3 Case-Study (FA, CC, GD, FK, YM, FP, IT, SP, DIR), pp. 20224–20231.
DATEDATE-2003-AraS #component #transaction #verification
A Proposal for Transaction-Level Verification with Component Wrapper Language (KA, KS), pp. 20082–20087.
DATEDATE-2003-CarbognaniLICB #modelling #precise #standard #using #verification
Qualifying Precision of Abstract SystemC Models Using the SystemC Verification Standard (FC, CKL, CNI, AC, PB), pp. 20088–20094.
DATEDATE-2003-GoldbergN #proving #satisfiability #verification
Verification of Proofs of Unsatisfiability for CNF Formulas (EIG, YN), pp. 10886–10891.
DATEDATE-2003-KnochelMHKA #simulation #verification
Verification of the RF Subsystem within Wireless LAN System Level Simulation (UK, TM, JH, RK, RA), pp. 20286–20291.
DATEDATE-2003-MounirMF #automation #behaviour #performance #verification
Automatic Behavioural Model Calibration for Efficient PLL System Verification (AM, AM, MF), pp. 20280–20285.
DATEDATE-2003-PastorP #concurrent #simulation #traversal #verification
Combining Simulation and Guided Traversal for the Verification of Concurrent Systems (EP, MAP), pp. 11158–11159.
DATEDATE-2003-SayintaCPAD #abstraction #case study #using #verification
A Mixed Abstraction Level Co-Simulation Case Study Using SystemC for System on Chip Verification (AS, GC, MP, AA, WD), pp. 20095–20100.
DATEDATE-2003-Zhou #verification
Timing Verification with Crosstalk for Transparently Latched Circuits (HZ), pp. 10056–10061.
ICDARICDAR-2003-BovinoIPS #multi #verification
Multi-Expert Verification of Hand-Written Signatures (LB, SI, GP, LS), pp. 932–936.
ICDARICDAR-2003-Fairhurst #authentication #documentation #future of #verification
Document Identity, Authentication and Ownership: The Future of Biometric Verification (MCF), p. 1108–?.
ICDARICDAR-2003-KameyaMO #online #sequence #verification
Figure-Based Writer Verification by Matching between an Arbitrary Part of Registered Sequence and an Input Sequence Extracted from On-Line Handwritten Figures (HK, SM, RO), pp. 985–989.
ICDARICDAR-2003-MoritaSBS #recognition #verification #word
A Recognition and Verification Strategy for Handwritten Word Recognition (MEM, RS, FB, CYS), p. 482–?.
ICDARICDAR-2003-PitrelliP #recognition #verification
Confidence-Scoring Post-Processing for Off-Line Handwritten-Character Recognition Verification (JFP, MPP), p. 278–?.
ICDARICDAR-2003-ShafieiR #algorithm #markov #modelling #online #segmentation #using #verification
A New On-Line Signature Verification Algorithm Using Variable Length Segmentation and Hidden Markov Models (MMS, HRR), p. 443–?.
ICDARICDAR-2003-Ueda #pattern matching #using #verification
Investigation of Off-Line Japanese Signature Verification Using a Pattern Matching (KU), p. 951–?.
ICDARICDAR-2003-YamazakiNK #markov #modelling #using #verification
Text-indicated Writer Verification Using Hidden Markov Models (YY, TN, NK), pp. 329–332.
ICDARICDAR-2003-ZimmerL #hybrid #verification
A Hybrid On/Off Line Handwritten Signature Verification System (AZ, LLL), pp. 424–428.
ICDARICDAR-2003-ZouTLL #analysis #online #using #verification
On-line Signature Verification Using Local Shape Analysis (MZ, JT, CL, ZL), pp. 314–318.
FASEFASE-2003-KochP #policy #specification #verification #visual notation
Visual Specifications of Policies and Their Verification (MK, FPP), pp. 278–293.
FASEFASE-2003-Kubica #approach #pointer #specification #verification
A Temporal Approach to Specification and Verification of Pointer Data-Structures (MK), pp. 231–245.
FoSSaCSFoSSaCS-2003-AbdullaR #communication #probability #verification
Verification of Probabilistic Systems with Faulty Communication (PAA, AMR), pp. 39–53.
FoSSaCSFoSSaCS-2003-AronsPZ #abstraction #probability #verification
Parameterized Verification by Probabilistic Abstraction (TA, AP, LDZ), pp. 87–102.
FoSSaCSFoSSaCS-2003-BlanchetP #encryption #protocol #termination #verification
Verification of Cryptographic Protocols: Tagging Enforces Termination (BB, AP), pp. 136–152.
FoSSaCSFoSSaCS-2003-FokkinkP #protocol #revisited #verification
Cones and Foci for Protocol Verification Revisited (WF, JP), pp. 267–281.
TACASTACAS-2003-BasuR #analysis #composition #verification
Compositional Analysis for Verification of Parameterized Systems (SB, CRR), pp. 315–330.
TACASTACAS-2003-BehrmannBFL #analysis #automaton #verification
Static Guard Analysis in Timed Automata Verification (GB, PB, EF, KGL), pp. 254–277.
TACASTACAS-2003-ChkliaevHV #protocol #verification
Verification and Improvement of the Sliding Window Protocol (DC, JH, EPdV), pp. 113–127.
TACASTACAS-2003-ClarkeFHKST #abstraction #hybrid #refinement #verification
Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement (EMC, AF, ZH, BHK, OS, MT), pp. 192–207.
TACASTACAS-2003-CobleighGP #composition #learning #verification
Learning Assumptions for Compositional Verification (JMC, DG, CSP), pp. 331–346.
TACASTACAS-2003-ZhangCS #analysis #concurrent #functional #performance #verification
The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems (DZ, RC, EWS), pp. 431–436.
IWPCIWPC-2003-GannodM #architecture #verification
Verification of Recovered Software Architectures (GCG, SM), pp. 258–265.
SASSAS-2003-AbadiB #email #protocol #verification
Computer-Assisted Verification of a Protocol for Certified Email (MA, BB), pp. 316–335.
SASSAS-2003-FieldGRY #abstraction #complexity #type system #verification
Typestate Verification: Abstraction Techniques and Complexity Results (JF, DG, GR, EY), pp. 439–462.
CIAACIAA-2003-FuBS #protocol #specification #verification
Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services (XF, TB, JS), pp. 188–200.
DLTDLT-2003-Esparza #approach #verification
An Automata-Theoretic Approach to Software Verification (JE), p. 21.
ICALPICALP-2003-XieDI #equation #infinity #polynomial #verification
A Solvable Class of Quadratic Diophantine Equations with Applications to Verification of Infinite-State Systems (GX, ZD, OHI), pp. 668–680.
FMFME-2003-AldiniB #approach #architecture #concurrent #verification
A General Approach to Deadlock Freedom Verification for Software Architectures (AA, MB), pp. 658–677.
FMFME-2003-BoyerS #constraints #protocol #synthesis #verification
Synthesis and Verification of Constraints in the PGM Protocol (MB, MS), pp. 264–281.
FMFME-2003-Holzmann #roadmap #verification
Trends in Software Verification (GJH), pp. 40–50.
FMFME-2003-KouchnarenkoL #component #refinement #verification
Refinement and Verification of Synchronized Component-Based Systems (OK, AL), pp. 341–358.
FMFME-2003-Rusu #composition #protocol #verification
Compositional Verification of an ATM Protocol (VR), pp. 223–243.
SEFMSEFM-2003-BeckertS #using #verification
Program Verification Using Change Information (BB, PHS), p. 91–?.
SEFMSEFM-2003-GawanmehTW #design #using #verification
Formal Verification of ASM Designs Using the MDG Tool (AG, ST, KW), pp. 210–219.
SEFMSEFM-2003-Xi #dependent type #verification
Facilitating Program Verification with Dependent Types (HX), pp. 72–81.
CHICHI-2003-CoventryAJ #interface #usability #verification
Usability and biometric verification at the ATM interface (LMC, ADA, GJ), pp. 153–160.
AdaEuropeAdaEurope-2003-BurnsL #verification
Adding Temporal Annotations and Associated Verification to Ravenscar Profile (AB, TML), pp. 80–91.
AdaSIGAda-2003-AmeyC #programming #verification
Static verification and extreme programming (PA, RC), pp. 4–9.
SEKESEKE-2003-LavazzaO #modelling #uml #verification
Simulation-based Verification of UML models (LL, GO), pp. 314–321.
SEKESEKE-2003-NetiniantiE #approach #aspect-oriented #using #verification
Adding Verification Property of Inter-Processes Using Aspect-Oriented Approach (PN, TE), pp. 54–60.
SIGIRSIGIR-2003-KhmelevT #categorisation #verification
A repetition based measure for verification of text collections and for text categorization (DVK, WJT), pp. 104–110.
LOPSTRLOPSTR-2003-BerghammerM #algorithm #approximate #development #using #verification
Formal Development and Verification of Approximation Algorithms Using Auxiliary Variables (RB, MMO), pp. 59–74.
PPDPPPDP-2003-Blanchet #approach #automation #encryption #logic programming #protocol #verification
Automatic verification of cryptographic protocols: a logic programming approach (BB), pp. 1–3.
RERE-2003-Catrava #quality #requirements #testing #towards #verification
Testing with Partial Traced Requirements: A Necessary Step Towards Higher Quality System Level Verification (SC), p. 303.
ESEC-FSEESEC-FSE-2003-GieseTBF #composition #design #realtime #towards #uml #verification
Towards the compositional verification of real-time UML designs (HG, MT, SB, SF), pp. 38–47.
ICSEICSE-2003-ChakiCGJV #c #component #composition #verification
Modular Verification of Software Components in C (SC, EMC, AG, SJ, HV), pp. 385–395.
ICSEICSE-2003-HatcliffDDJR #analysis #component #development #named #verification
Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems (JH, XD, MBD, GJ, VPR), pp. 160–173.
HPCAHPCA-2003-GassendSCDD #memory management #performance #verification
Caches and Hash Trees for Efficient Memory Integrity Verification (BG, GES, DEC, MvD, SD), pp. 295–306.
CAVCAV-2003-BeyerLN #named #realtime #verification
Rabbit: A Tool for BDD-Based Verification of Real-Time Systems (DB, CL, AN), pp. 122–125.
CAVCAV-2003-BozgaLP #automation #named #protocol #security #verification
HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols (LB, YL, MP), pp. 219–222.
CAVCAV-2003-LahiriB #deduction #verification
Deductive Verification of Advanced Out-of-Order Microprocessors (SKL, REB), pp. 341–353.
CAVCAV-2003-MouraRS #bound #induction #model checking #verification
Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A) (LMdM, HR, MS), pp. 14–26.
CAVCAV-2003-XieDIP #problem #verification
Dense Counter Machines and Verification Problems (GX, ZD, OHI, PSP), pp. 93–105.
CSLCSL-2003-Bouajjani #infinity #tutorial #verification
Verification of Infinite State Systems (Tutorial) (AB), p. 71.
CSLCSL-2003-Veith #community #verification
Friends or Foes? Communities in Software Verification (Invited Lecture) (HV), pp. 528–529.
ICLPICLP-2003-DelzannoGM #composition #infinity #verification
Compositional Verification of Infinite State Systems (GD, MG, MCM), pp. 47–48.
ICLPICLP-2003-KingL #logic programming #source code #verification
Forward versus Backward Verification of Logic Programs (AK, LL), pp. 315–330.
LICSLICS-2003-Harrison #verification
Formal Verification at Intel (JH), p. 45–?.
LICSLICS-2003-NeculaS #framework #generative
A Sound Framework for Untrusted Verification-Condition Generators (GCN, RRS), pp. 248–260.
ICSTSAT-2003-ClarkeTVW #abstraction #hardware #satisfiability #verification
SAT Based Predicate Abstraction for Hardware Verification (EMC, MT, HV, DW), pp. 78–92.
VMCAIVMCAI-2003-Cousot #abstract interpretation #automation #verification
Automatic Verification by Abstract Interpretation (PC), pp. 20–24.
VMCAIVMCAI-2003-OgataF #protocol #verification
Formal Verification of the Horn-Preneel Micropayment Protocol (KO, KF), pp. 238–252.
VMCAIVMCAI-2003-Wang #automaton #performance #verification
Efficient Verification of Timed Automata with BDD-Like Data-Structures (FW), pp. 189–205.
CBSECBSE-2003-MehlitzP #design pattern #reliability #using #verification
Design for Verification: Using Design Patterns to Build Reliable Systems (PCM, JJP), p. 10.
ASEASE-2002-CalderM #automation #communication #concurrent #process #verification
Automatic Verification of any Number of Concurrent, Communicating Processes (MC, AM), pp. 227–230.
ASEASE-2002-CsertanHMPPV #automation #modelling #named #uml #validation #verification #visual notation
VIATRA — Visual Automated Transformations for Formal Verification and Validation of UML Models (GC, GH, IM, ZP, AP, DV), pp. 267–270.
ASEASE-2002-GiannakopoulouPB #component #generative #verification
Assumption Generation for Software Component Verification (DG, CSP, HB), pp. 3–12.
ASEASE-2002-LiKF #composition #interface #verification
Interfaces for Modular Feature Verification (HCL, SK, KF), pp. 195–204.
DACDAC-2002-BartleyGB #comparison #pseudo #random testing #testing #verification
A comparison of three verification techniques: directed testing, pseudo-random testing and property checking (MB, DG, TB), pp. 819–823.
DACDAC-2002-ChakrabartiDCB #interface #realtime #specification #verification
Formal verification of module interfaces against real time specifications (AC, PD, PPC, AB), pp. 141–145.
DACDAC-2002-ChangC #implementation #self #verification
Self-referential verification of gate-level implementations of arithmetic circuits (YTC, KTC), pp. 311–316.
DACDAC-2002-DillJRBFFRSW #verification
Formal verification methods: getting around the brick wall (DLD, NJ, SR, GB, LF, HF, RKR, GS, CW), pp. 576–577.
DACDAC-2002-EderB #logic #performance #pipes and filters #verification
Achieving maximum performance: a method for the verification of interlocked pipeline control logic (KE, GB), pp. 135–140.
DACDAC-2002-HartongHB #algorithm #model checking #verification
Model checking algorithms for analog verification (WH, LH, EB), pp. 542–547.
DACDAC-2002-HazelhurstWKF #approach #design #hybrid #verification
A hybrid verification approach: getting deep into the design (SH, OW, GK, LF), pp. 111–116.
DACDAC-2002-LeeKK #named #verification
VeriCDF: a new verification methodology for charged device failures (JL, KWK, SMK), pp. 874–879.
DATEDATE-2002-BlasquezHFLBHB #industrial #verification
Formal Verification Techniques: Industrial Status and Perspectives (JB, MvH, AF, JLL, DB, CH, PB), p. 1050.
DATEDATE-2002-CiesielskiKZR #canonical #diagrams #representation #verification
Taylor Expansion Diagrams: A Compact, Canonical Representation with Applications to Symbolic Verification (MJC, PK, ZZ, BR), pp. 285–289.
DATEDATE-2002-FerrandiRS #constraints #functional #theorem proving #using #verification
Functional Verification for SystemC Descriptions Using Constraint Solving (FF, MR, DS), pp. 744–751.
DATEDATE-2002-JerkeL #analysis #verification
Hierarchical Current Density Verification for Electromigration Analysis in Arbitrary Shaped Metallization Patterns of Analog Circuits (GJ, JL), pp. 464–469.
DATEDATE-2002-KaivolaN #float #multi #verification
Formal Verification of the Pentium ® 4 Floating-Point Multiplier (RK, NN), pp. 20–27.
DATEDATE-2002-MishraDNT #automation #execution #functional #multi #pipes and filters #verification
Automatic Verification of In-Order Execution In Microprocessors with Fragmented Pipelines and Multicycle Functional Units (PM, NDD, AN, HT), pp. 36–43.
DATEDATE-2002-PenaCSP #case study #verification
A Case Study for the Verification of Complex Timed Circuits: IPCMOS (MAP, JC, ABS, EP), pp. 44–51.
DATEDATE-2002-StohrSG #named #reuse #verification
FlexBench: Reuse of Verification IP to Increase Productivity (BS, MS, JG), p. 1131.
ESOPESOP-2002-FlanaganFQ #source code #thread #verification
Thread-Modular Verification for Shared-Memory Programs (CF, SNF, SQ), pp. 262–277.
FASEFASE-2002-BartheGH #composition #interactive #verification
Compositional Verification of Secure Applet Interactions (GB, DG, MH), pp. 15–32.
FASEFASE-2002-DavidMY #realtime #uml #verification
Formal Verification of UML Statecharts with Real-Time Extensions (AD, MOM, WY), pp. 218–232.
FoSSaCSFoSSaCS-2002-Abraham-MummBRS #concept #java #multi #thread #verification
Verification for Java’s Reentrant Multithreading Concept (EÁM, FSdB, WPdR, MS), pp. 5–20.
TACASTACAS-2002-BozzanoD #verification
Beyond Parameterized Verification (MB, GD), pp. 221–235.
TACASTACAS-2002-BrabermanGO #using #verification
Improving the Verification of Timed Systems Using Influence Information (VAB, DG, AO), pp. 21–36.
TACASTACAS-2002-DelzannoRB #automation #java #parallel #source code #thread #towards #verification
Towards the Automated Verification of Multithreaded Java Programs (GD, JFR, LVB), pp. 173–187.
TACASTACAS-2002-KimSC #functional #requirements #specification #using #verification
Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS (TK, DWJSC, SDC), pp. 205–220.
TACASTACAS-2002-Lang #composition #using #verification
Compositional Verification Using SVL Scripts (FL), pp. 465–469.
WRLAWRLA-2002-OgataF #authentication #protocol #verification
Rewriting-Based Verification of Authentication Protocols (KO, KF), pp. 208–222.
PLDIPLDI-2002-DasLS #named #polynomial #verification
ESP: Path-Sensitive Program Verification in Polynomial Time (MD, SL, MS), pp. 57–68.
SASSAS-2002-CorinE #constraints #protocol #security #verification
An Improved Constraint-Based System for the Verification of Security Protocols (RC, SE), pp. 326–341.
SASSAS-2002-Yavuz-KahveciB #automation #concurrent #verification
Automated Verification of Concurrent Linked Lists with Counters (TYK, TB), pp. 69–84.
CIAACIAA-J-2000-Ibarra02 #multi #verification
Verification in Queue-Connected Multicounter Machines (OHI), pp. 115–127.
CIAACIAA-2002-BartzisB #automation #constraints #verification
Automata-Based Representations for Arithmetic Constraints in Automated Verification (CB, TB), pp. 282–288.
DLTDLT-2002-IbarraDS #automaton #finite #safety #verification
Safety Verification for Two-Way Finite Automata with Monotonic Counters (OHI, ZD, ZWS), pp. 326–338.
FMFME-2002-FirleyG #abstraction #verification
Property Dependent Abstraction of Control Structure for Software Verification (TF, UG), pp. 511–530.
FMFME-2002-GaravelH #evaluation #functional #on the #performance #using #verification
On Combining Functional Verification and Performance Evaluation Using CADP (HG, HH), pp. 410–429.
FMFME-2002-HendersonP #classification #communication #verification
The Formal Classification and Verification of Simpson’s 4-Slot Asynchronous Communication Mechanism (NH, SP), pp. 350–369.
FMFME-2002-Rusu #generative #testing #using #verification
Verification Using Test Generation Techniques (VR), pp. 252–271.
IFMIFM-2002-NepomniaschySBK #approach #design #distributed #named #specification #verification
Basic-REAL: Integrated Approach for Design, Specification and Verification of Distributed Systems (VAN, NVS, EVB, VEK), pp. 69–88.
CAiSECAiSE-2002-BenerecettiPST #model checking #multi #protocol #verification
Verification of Payment Protocols via MultiAgent Model Checking (MB, MP, LS, ST), pp. 311–327.
EDOCEDOC-2002-KoehlerTK #consistency #implementation #process #verification
From Business Process Model to Consistent Implementation: A Case for Formal Verification Methods (JK, GT, SK), p. 96–?.
ICEISICEIS-2002-MatsuuraI #generative #verification
Digital Timestamps for Dispute Settlement in Electronic Commerce: Generation, Verification, and Renewal (KM, HI), pp. 962–967.
ICEISICEIS-2002-PantiSTV #automation #protocol #security #verification
Automatic Verification of Security in Payment Protocols for Electronic Commerce (MP, LS, ST, SV), pp. 968–974.
ICPRICPR-v1-2002-ZhangW #algorithm #verification
Core-Based Structure Matching Algorithm of Fingerprint Verification (WZ, YW), pp. 70–74.
ICPRICPR-v2-2002-CzyzKV #verification
Combining Face Verification Experts (JC, JK, LV), pp. 28–31.
ICPRICPR-v2-2002-FangTW #verification
Fusion of Global and Local Features for Face Verification (YF, TT, YW), pp. 382–385.
ICPRICPR-v2-2002-MarcelB #using #verification
Improving Face Verification Using Skin Color Information (SM, SB), pp. 378–381.
ICPRICPR-v3-2002-CeguerraK #automation #verification
Integrating Local and Global Features in Automatic Fingerprint Verification (AC, IK), pp. 347–350.
ICPRICPR-v3-2002-HatanoASMOOK #algorithm #difference #using #verification
A Fingerprint Verification Algorithm Using the Differential Matching Rate (TH, TA, SS, HM, SO, YO, HK), pp. 799–802.
ICPRICPR-v3-2002-MaioMCWJ #contest #named #verification
FVC2002: Second Fingerprint Verification Competition (DM, DM, RC, JLW, AKJ), pp. 811–814.
ICPRICPR-v3-2002-PankantiRB #case study #fault #verification
Structure in Errors: A Case Study in Fingerprint Verification (SP, NKR, RMB), pp. 440–447.
KDDKDD-2002-ChungC #clustering #cvs #information retrieval #named
CVS: a Correlation-Verification based Smoothing technique on information retrieval and term clustering (CYC, BC), pp. 469–474.
SEKESEKE-2002-SciascioDMP #automation #named #verification #web
AnWeb: a sytem for automatic support to web application verification (EDS, FMD, MM, GP), pp. 609–616.
LOPSTRLOPSTR-2002-Martin-MateosAHR #framework #verification
Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers (FJMM, JAA, MJH, JLRR), pp. 182–198.
PPDPPPDP-2002-BozzanoD #automation #linear #logic #protocol #verification
Automated protocol verification in linear logic (MB, GD), pp. 38–49.
POPLPOPL-2002-FlanaganQ #abstraction #verification
Predicate abstraction for software verification (CF, SQ), pp. 191–202.
RERE-2002-DuranCCT #requirements #using #verification
Supporting Requirements Verification Using XSLT (AD, ARC, RC, MT), pp. 165–172.
SACSAC-2002-Abu-GhazalehP #execution #mobile #performance #towards #verification
Verification caching: towards efficient and secure mobile code execution environments (NBAG, DSP), pp. 964–968.
SACSAC-2002-HoomanP #architecture #distributed #replication #verification
Formal verification of replication on a distributed data space architecture (JH, JvdP), pp. 351–358.
ICSEICSE-2002-DengDHM #concurrent #invariant #source code #specification #synthesis #verification
Invariant-based specification, synthesis, and verification of synchronization in concurrent programs (XD, MBD, JH, MM), pp. 442–452.
ICSEICSE-2002-EshuisW #design #graph #process #uml #verification #workflow
Verification support for workflow design with UML activity graphs (RE, RW), pp. 166–176.
ICSEICSE-2002-RoychoudhuryM #java #parallel #semantics #specification #thread #verification