93 papers:
PLDI-2015-Carbonneaux0S #bound #composition- Compositional certified resource bounds (QC, JH, ZS), pp. 467–478.
FM-2015-SharmaWCHC #infinity #reasoning- Certified Reasoning with Infinity (AS, SW, AC, AH, WNC), pp. 496–513.
ICFP-2015-BahrBE #contract #multi- Certified symbolic management of financial multi-party contracts (PB, JB, ME), pp. 315–327.
KDD-2015-FeldmanFMSV- Certifying and Removing Disparate Impact (MF, SAF, JM, CS, SV), pp. 259–268.
POPL-2015-GuKRSWWZG #abstraction #specification- Deep Specifications and Certified Abstraction Layers (RG, JK, TR, ZS, X(W, SCW, HZ, YG), pp. 595–608.
SOSP-2015-ChenZCCKZ #file system #hoare #logic #using- Using Crash Hoare logic for certifying the FSCQ file system (HC, DZ, TC, AC, MFK, NZ), pp. 18–37.
RTA-2015-NageleZ- Certified Rule Labeling (JN, HZ), pp. 269–284.
SAS-2014-BessonJV #java #named #static analysis- SawjaCard: A Static Analysis Tool for Certifying Java Card Applications (FB, TPJ, PV), pp. 51–67.
CIKM-2013-BagdouriWLO #classification #towards- Towards minimizing the annotation cost of certified text classification (MB, WW, DDL, DWO), pp. 989–998.
ICST-2013-LegeardB #enterprise #modelling #testing- Smartesting CertifyIt: Model-Based Testing for Enterprise IT (BL, AB), pp. 391–397.
STOC-2012-VaziraniV #generative #quantum #random- Certifiable quantum dice: or, true random number generation secure against quantum adversaries (UVV, TV), pp. 61–76.
ICALP-v1-2012-Schmidt #linear- Certifying 3-Connectivity in Linear Time (JMS), pp. 786–797.
- FM-2012-CarlierDG #constraints #finite #theorem proving
- A Certified Constraint Solver over Finite Domains (MC, CD, AG), pp. 116–131.
- POPL-2012-StrubSFC #coq #named #self
- Self-certification: bootstrapping certified typecheckers in F* with Coq (PYS, NS, CF, JC), pp. 571–584.
PLEASE-2012-SozenM #adaptation #product line- Adapting software product lines for complex certifiable avionics software (NS, EM), pp. 21–24.
SIGMOD-2011-ChenDLS #challenge- We challenge you to certify your updates (SC, XLD, LVSL, DS), pp. 481–492.
CAV-2011-AlkassarBMR #verification- Verification of Certifying Computations (EA, SB, KM, CR), pp. 67–82.
- RTA-2011-ContejeanCFPU #automation #proving
- Automated Certified Proofs with CiME3 (EC, PC, JF, OP, XU), pp. 21–30.
- RTA-2011-SternagelT #composition #semantics
- Modular and Certified Semantic Labeling and Unlabeling (CS, RT), pp. 329–344.
TACAS-2010-DragerKFW #concurrent #infinity #model checking #named- SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems (KD, AK, BF, HW), pp. 271–274.
ICSM-2010-AbdallahMG #robust #slicing #using- Certifying software robustness using program slicing (MA, MM, KG), pp. 1–2.
PEPM-2010-ContejeanPUCPF #approach #automation #proving #termination- A3PAT, an approach for certified automated termination proofs (EC, AP, XU, PC, OP, JF), pp. 63–72.
IFM-2010-DiosMP #pointer- Certified Absence of Dangling Pointers in a Language with Explicit Deallocation (JdD, MM, RP), pp. 305–319.
- IFM-2010-Stratulat #induction #proving
- Integrating Implicit Induction Proofs into Certified Proof Environments (SS), pp. 320–335.
- ICFP-2010-McCreightCT #compilation #framework #garbage collection
- A certified framework for compiling and executing garbage-collected languages (AM, TC, APT), pp. 273–284.
ICSE-2010-KumarSS #for free- Can we certify systems for freedom from malware (NVNK, HJS, RKS), pp. 175–178.
- RTA-2010-SternagelT
- Certified Subterm Criterion and Certified Usable Rules (CS, RT), pp. 325–340.
- FM-2009-LuthW #c #source code #specification #verification
- Certifiable Specification and Verification of C Programs (CL, DW), pp. 419–434.
CSMR-2008-SneedO #maintenance- Training and Certifying Software Maintainers (HMS, SO), pp. 113–122.
- PLDI-2008-FengSDG #hardware #low level #source code #thread
- Certifying low-level programs with hardware interrupts and preemptive threads (XF, ZS, YD, YG), pp. 170–182.
FLOPS-2008-Julien #induction #integer #using- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base (NJ), pp. 48–63.
PADL-2008-PaganoACCCMW #development #implementation #ml #tool support- Certified Development Tools Implementation in Objective Caml (BP, OA, BC, EC, JLC, TM, PW), pp. 2–17.
SAC-2008-AndronickN #embedded #protocol- Certifying an embedded remote method invocation protocol (JA, QHN), pp. 352–359.
IJCAR-2008-BoyerGJ #automaton- Certifying a Tree Automata Completion Checker (BB, TG, TPJ), pp. 523–538.
ESOP-2007-BarthePR #bytecode #java #lightweight #verification- A Certified Lightweight Non-interference Java Bytecode Verifier (GB, DP, TR), pp. 125–140.
- PLDI-2007-CaiSV #self
- Certified self-modifying code (HC, ZS, AV), pp. 66–77.
- PLDI-2007-Chlipala #assembly #compilation #λ-calculus
- A certified type-preserving compiler from λ calculus to assembly language (AC), pp. 54–65.
- PLDI-2007-McCreightSLL #framework #garbage collection
- A general framework for certifying garbage collectors and their mutators (AM, ZS, CL, LL), pp. 468–479.
MoDELS-2007-ChakiILWZ #modelling- Model-Driven Construction of Certified Binaries (SC, JI, PL, KCW, NZ), pp. 666–681.
- MoDELS-2007-ChakiILWZ #modelling
- Model-Driven Construction of Certified Binaries (SC, JI, PL, KCW, NZ), pp. 666–681.
- SAC-2007-BonenfantCHMWW #cost analysis #towards
- Towards resource-certified software: a formal cost model for time and its application to an image-processing example (AB, ZC, KH, GM, AMW, IW), pp. 1307–1314.
- SAC-2007-Hamid #memory management #runtime
- Integrating a certified memory management runtime with proof-carrying code (NAH), pp. 1526–1533.
COCV-2007-BlechP #code generation- A Certifying Code Generation Phase (JOB, APH), pp. 65–82.
CADE-2007-Krauss #termination- Certified Size-Change Termination (AK), pp. 460–475.
DATE-2006-NakamuraST #integration #performance #simulation- An efficient and portable scheduler for RTOS simulation and its certified integration to SystemC (HN, NS, NT), pp. 1157–1158.
- FM-2006-DelahayeED #security #using
- Certifying Airport Security Regulations Using the Focal Environment (DD, JFÉ, VDG), pp. 48–63.
- ICFP-2006-Chlipala #composition #development #proving #verification
- Modular development of certified program verifiers with a proof assistant (AC), pp. 160–171.
- POPL-2006-NiS #assembly #embedded #pointer #programming
- Certified assembly programming with embedded code pointers (ZN, ZS), pp. 320–333.
- IJCAR-2006-GregoireT #composition #functional #library #scalability
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers (BG, LT), pp. 423–437.
- RTA-2006-Koprowski #higher-order #recursion
- Certified Higher-Order Recursive Path Ordering (AK), pp. 227–241.
VMCAI-2006-ChangCN #framework #program analysis #safety- A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety (BYEC, AC, GCN), pp. 174–189.
- SAS-2005-HarrenN #assembly #dependent type #safety #using
- Using Dependent Types to Certify the Safety of Assembly Code (MH, GCN), pp. 155–170.
CIAA-J-2004-GeserHWZ05 #automaton #finite #string #term rewriting #termination- Finding finite automata that certify termination of string rewriting systems (AG, DH, JW, HZ), pp. 471–486.
- FM-2005-CacheraJPS #analysis #memory management
- Certified Memory Usage Analysis (DC, TPJ, DP, GS), pp. 91–106.
GPCE-2005-DenneyF #generative- Certifiable Program Generation (ED, BF), pp. 17–28.
- CADE-2005-Benedetti #named
- sKizzo: A Suite to Evaluate and Certify QBFs (MB), pp. 369–376.
LICS-2005-JiaSWG #compilation #stack- Certifying Compilation for a Language with Stack Allocation (LJ, FS, DW, NG), pp. 407–416.
- RTA-2005-GeserHWZ #automaton #linear #on the #term rewriting #termination
- On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems (AG, DH, JW, HZ), pp. 353–367.
FASE-2004-BartheD #bytecode #framework #verification- A Tool-Assisted Framework for Certified Bytecode Verification (GB, GD), pp. 99–113.
- CIAA-2004-GeserHWZ #automaton #finite #string #termination
- Finding Finite Automata That Certify Termination of String Rewriting (AG, DH, JW, HZ), pp. 134–145.
- POPL-2004-Rival #compilation
- Symbolic transfer function-based approaches to certified compilation (XR), pp. 1–13.
- SAC-2004-NenadicZB #email
- Fair certified e-mail delivery (AN, NZ, SB), pp. 391–396.
- IJCAR-2004-DenneyFS #automation #proving #theorem proving #using
- Using Automated Theorem Provers to Certify Auto-generated Aerospace Software (ED, BF, JS), pp. 198–212.
- RTA-2004-Contejean #algorithm
- A Certified AC Matching Algorithm (EC), pp. 70–84.
- VMCAI-2004-XiaH #c #source code
- Certifying Temporal Properties for Compiled C Programs (SX, JH), pp. 161–174.
ASE-2003-RosuC #metric #safety- Certifying Measurement Unit Safety Polic (GR, FC), pp. 304–309.
- DATE-2003-LaurentK #validation
- A System to Validate and Certify Soft and Hard IP (BL, TK), pp. 20208–20213.
- ESOP-2003-YuHS #library
- Building Certified Libraries for PCC: Dynamic Storage Allocation (DY, NAH, ZS), pp. 363–379.
- SAS-2003-AbadiB #email #protocol #verification
- Computer-Assisted Verification of a Protocol for Certified Email (MA, BB), pp. 316–335.
- FME-2003-RosuELM #equation #proving
- Certifying and Synthesizing Membership Equational Proofs (GR, SE, PL, JM), pp. 359–380.
- CADE-2003-CohenMPS #permutation #problem
- Certifying Solutions to Permutation Group Problems (AMC, SHM, MP, VS), pp. 258–273.
- CADE-2003-CraryS #framework #logic
- Foundational Certified Code in a Metalogical Framework (KC, SS), pp. 106–120.
- CAV-2003-RosuVWL #estimation #source code
- Certifying Optimality of State Estimation Programs (GR, RPV, JW, LL), pp. 301–314.
- ASE-2002-RosuW #towards
- Towards Certifying Domain-Specific Properties of Synthesized Code (GR, JW), pp. 289–294.
- PLDI-2002-RamalingamWFGS #analysis #component #consistency
- Deriving Specialized Program Analyses for Certifying Component-Client Conformance (GR, AV, JF, DG, SS), pp. 83–94.
- FME-2002-WhalenSF
- Synthesizing Certified Code (MWW, JS, BF), pp. 431–450.
- ICFP-2002-CraryV #scalability #type system
- An expressive, scalable type theory for certified code (KC, JV), pp. 191–205.
- POPL-2002-ShaoSTP #type system
- A type system for certified binaries (ZS, BS, VT, NP), pp. 217–232.
- LICS-2002-Atserias #random #satisfiability
- Unsatisfiable Random Formulas Are Hard to Certify (AA), pp. 325–334.
TestCom-2002-CastanetR #analysis #proving #reachability #testing #theorem proving- Generate Certified Test Cases by Combining Theorem Proving and Reachability Analysis (RC, DR), pp. 249–266.
- ASE-2001-LowryPR #policy
- Certifying Domain-Specific Policies (MRL, TP, GR), pp. 81–90.
- CAV-2001-Namjoshi #model checking
- Certifying Model Checkers (KSN), pp. 2–13.
- PLDI-2000-ColbyLNBPC #compilation #java
- A certifying compiler for Java (CC, PL, GCN, FB, MP, KC), pp. 95–107.
- PEPM-1999-HornofJ #code generation #compilation #runtime
- Certifying Compilation and Run-Time Code Generation (LH, TJ), pp. 60–74.
- PLDI-1998-NeculaL #compilation #design #implementation
- The Design and Implementation of a Certifying Compiler (GCN, PL), pp. 333–344.
- SAS-1998-Lee #compilation #optimisation
- Certifying, Optimizing Compilation (Abstract) (PL0), p. 381.
- Best-of-PLDI-1998-NeculaL98a #compilation #design #implementation
- The design and implementation of a certifying compiler (with retrospective) (GCN, PL), pp. 612–625.
- CADE-1998-Thery #algorithm
- A Certified Version of Buchberger’s Algorithm (LT), pp. 349–364.
ICDAR-1993-LoprestiS #recognition- Certifiable optical character recognition (DPL, JSS), pp. 432–435.
DAC-1992-DevadasKMW #logic #verification- Certified Timing Verification and the Transition Delay of a Logic Circuit (SD, KK, SM, ARW), pp. 549–555.
- STOC-1986-GoldwasserK
- Almost All Primes Can Be Quickly Certified (SG, JK), pp. 316–329.
- POPL-1986-LengauerH #concurrent #network #sorting #theorem
- A Mechanically Certified Theorem about Optimal Concurrency of Sorting Networks (CL, CHH), pp. 307–317.
- POPL-1979-ReitmanA #approach #axiom #data flow #source code
- Certifying Information Flow Properties of Programs: An Axiomatic Approach (RPR, GRA), pp. 283–290.
