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:
code (11)
program (11)
compil (10)
system (8)
proof (7)

Stem certifi$ (all stems)

93 papers:

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

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.