Unsummarized papers are at the end.

Summarized papers

Serberus: Protecting Cryptographic Code from Spectres at Compile-Time [mosier:sandp:2023]
Automating constraint-aware datapath optimization using E-graphs [coward:arxiv:2023]
End-to-end formal verification of a RISC-V processor extended with capability pointers [gao:fmcad:2021]
Opening Pandora's box: A systematic study of new ways microarchitecture can leak private data [vicarte:isca:2021]
The fallacy of spec-based design [bhatt:sefm:2003]
The tensor algebra compiler [kjolstad:oopsla:2017]
Sparse GPU kernels for deep learning [gale:arxiv:2020]
The state of sparsity in deep neural networks [gale:arxiv:2019]
Fast sparse ConvNets [elsen:arxiv:2019]
TensorFlow: Large-scale machine learning on heterogeneous distributed systems [abadi:arxiv:2016]
In-datacenter performance analysis of a tensor processing unit [jouppi:isca:2017]
SIGMA: A sparse and irregular GEMM accelerator with flexible interconnects for DNN training [qin:hpca:2020]
ExTensor: An accelerator for sparse tensor algebra [hedge:micro:2019]
Attention is all you need [vaswani:arxiv:2017]
Outrageously large neural networks: The sparsely-gated mixture-of-experts layer [shazeer:arxiv:2017]
GShard: Scaling giant models with conditional computation and automatic sharding [lepikhin:arxiv:2020]
Switch transformers: Scaling to trillion parameter models with simple and efficient sparsity [fedus:arxiv:2021]
GeST: An automatic framework for generating CPU stress-tests [hadjilambrou:ispass:2019]
Silent data corruptions at scale [dixit:arxiv:2021]
Cores that don't count [hochschild:hotos:2021]
CHERI concentrate: Practical compressed capabilities [woodruff:tocs:2019]
The next 700 semantics: A research challenge [krishnamurthi:snapl:2019]
snmalloc: A message passing allocator [lietar:ismm:2019]
CacheQuery: Learning replacement policies from hardware caches [vila:pldi:2020]
PAC: Practical accountability for CCF [shamis:arxiv:2021]
Toward confidential cloud computing: Extending hardware-enforced cryptographic protection to data while in use [russinovich:acmq:2021]
Spectector: Principled detection of speculative information flows [guarnieri:sandp:2020]
Phantom types and subtyping [fluet:jfp:2006]
GhostCell: Separating permissions from data in Rust [yanovski:unknown:2021]
Understanding memory and thread safety practices and issues in real-world Rust programs [qin:pldi:2020]
How do programmers use unsafe Rust? [astrauskas:oopsla:2020]
Is Rust used safely by software developers? [evans:icse:2020]
Checking type safety of foreign function calls [furr:pldi:2005]
Dependent types for low-level programming [condit:esop:2007]
QSYM: A practical concolic execution engine tailored for hybrid fuzzing [yun:usenix:2018]
Symbolic execution with SymCC: Don't interpret, compile! [poeplau:usenix:2020]
SAVIOR: Towards bug-driven hybrid testing [chen:sp:2020]
TracerX: Dynamic symbolic execution with interpolation [jaffar:arxiv:2020]
Practical, low-effort equivalence verification of real code [ramos:cav:2011]
A local shape analysis based on separation logic [distefano:tacas:2006]
Beyond reachability: Shape abstraction in the presence of pointer arithmetic [calcagno:sas:2006]
Noninterference for free [bowman:icfp:2015]
Generalized symbolic execution for model checking and testing [khurshid:tacas:2003]
Scalable error detection using boolean satisfiability [xie:popl:2005]
Under-constrained symbolic execution: Correctness checking for real code [ramos:sec:2015]
Quantifying the performance of garbage collection vs. explicit memory management [hertz:oopsla:2005]
Under-constrained execution: Making automatic code destruction easy and scalable [engler:issta:2007]
Engineering the Servo web browser engine using Rust [anderson:icse:2016]
Formal specification and testing of QUIC [mcmillan:sigcomm:2019]
Executable counterexamples in software model checking [gennari:vstte:2018]
The meaning of memory safety [azevedo:post:2018]
Large teams have developed science and technology; small teams have disrupted it [wu:arxiv:2017]
A segmented memory model for symbolic execution [kapus:fse:2019]
Rethinking pointer reasoning in symbolic execution [coppa:ase:2017]
Safe systems programming in Rust: The promise and the challenge [jung:cacm:2021]
Swarm verification techniques [holzmann:ieeetse:2011]
Swarm testing [groce:issta:2012]
Chopped symbolic execution [trabish:icse:2018]
Scaling symbolic execution using ranged analysis [siddiqui:oopsla:2012]
A synergistic approach for distributed symbolic execution using test ranges [qiu:icse:2017]
Efficient state merging in symbolic execution [kuznetsov:pldi:2012]
Sanity checks in formal verification [kupferman:concur:2006]
Evaluating manual intervention to address the challenges of bug finding with KLEE [galea:arxiv:2018]
Finding code that explodes under symbolic evaluation [bornholt:oopsla:2018]
As we may think [bush:atlantic:1945]
Modern code review: A case study at Google [sadowski:icse-seip:2018]
Lessons from building static analysis tools at Google [sadowski:cacm:2018]
Large-scale automated refactoring using ClangMR [wright:icsm:2013]
Tricorder: Building a program analysis ecosystem [sadowski:icse:2015]
Why Google stores billions of lines of code in a single repository [potvin:cacm:2016]
API usability at scale [macvean:ppig:2016]
Spanner: Google's globally distributed database [corbett:tocs:2013]
Extended static checking: A ten-year perspective [leino:informatics:2001]
QuickCheck: A lightweight tool for random testing of Haskell programs [claessen:icfp:2000]
Parameterized unit tests [tillmann:fse:2005]
Feedback-directed unit test generation for C/C++ using concolic execution [garg:icse:2013]
Study of integrating random and symbolic testing for object-oriented software [dimjasevic:ifm:2018]
FUDGE: Fuzz driver generation at scale [babic:fse:2019]
DeepState: Symbolic unit testing for C and C++ [goodman:ndss:2018]
Locating defects is uncertain [zeller:bugs:2005]
Soundness and its role in bug detection systems [xie:bugs:2005]
The soundness of bugs is what matters (position statement) [godefroid:bugs:2005]
Issues in deploying software defect detection tools [cok:bugs:2005]
False positives over time: A problem in deploying static analysis tools [chou:bugs:2005]
The human in formal methods [krishnamurthi:fm:2019]
Relational test tables: A practical specification language for evolution and security [weigl:arxiv:2019]
COASTAL: Combining concolic and fuzzing for Java (competition contribution) [visser:tacas:2020]
SUSHI: A test generator for programs with complex structured inputs [braione:icse:2018]
STARS: Rise and fall of minicomputers [scanning our past] [bell:procieee:2014]
Bell's law for the birth and death of computer classes [bell:cacm:2008]
Software model checking [jhala:compsurv:2009]
Boolean satisfiability from theoretical hardness to practical success [malik:cacm:2009]
Test-case reduction via test-case generation: Insights from the Hypothesis reducer [maciver:ecoop:2020]
Model checking: Algorithmic verification and debugging [clarke:cacm:2009]
Enhancing symbolic execution with veritesting [avgerinos:icse:2014]
Code-level model checking in the software development workflow [chong:icse:2020]
An empirical study of the reliability of UNIX utilities [miller:cacm:1990]
Selective symbolic execution [chipounov:hotdep:2009]
The art, science, and engineering of fuzzing: A survey [manes:ieeetse:2019]
Fuzzing: Hack, art, and science [godefroid:cacm:2020]
Symbolic execution for software testing: Three decades later [cadar:cacm:2013]
A survey of symbolic execution techniques [baldoni:compsurv:2018]
Fuzzing: On the exponential cost of vulnerability discovery [bohme2:fse:2020]
An introduction to test specification in FQL [holzer:hvc:2010]
FShell: Systematic test case generation for dynamic analysis and measurement [holzer:cav:2008]
Satisfiability modulo theories: Introduction and applications [demoura:cacm:2011]
Software verification: Testing vs. model checking [beyer:hvc:2017]
TestCov: Robust test-suite execution and coverage measurement [beyer:ase:2019]
Boosting fuzzer efficiency: An information theoretic perspective [bohme:fse:2020]
Model checking [mcmillan:ecs:2003]
Verification of safety functions implemented in Rust: A symbolic execution based approach [lindner:indin:2019]
No panic! Verification of Rust programs by symbolic execution [lindner:indin:2018]
Simple verification of Rust programs via functional purification [ullrich:msc:2016]
RustHorn: CHC-based verification for Rust programs [matsushita:esop:2020]
Benchmarking solvers, SAT-style [nyxbrain:sc2:2017]
Fractional permissions without the fractions [heule:ftfjp:2011]
StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities [skorstengaard:popl:2019]
Dafny: An automatic program verifier for functional correctness [leino:lpair:2010]
The Boogie verification debugger [legoues:sefm:2011]
The ramifications of sharing in data structures [hobor:popl:2013]
Developing verified programs with Dafny [leino:icse:2013]
Reasoning about a machine with local capabilities [skorstengaard:esop:2018]
Specified blocks [hehner:vstte:2008]
Local reasoning about while-loops [tuerk:vstte:2010]
Verifying event-driven programs using ramified frame properties [krishnaswami:tldi:2010]
Specification and verification: The Spec# experience [barnett:cacm:2011]
Separation logic and abstraction [parkinson:popl:2005]
Verification of concurrent programs with Chalice [leino:fosad:2007]
Compositional shape analysis by means of bi-abduction [calcagno:popl:2009]
Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
Symbolic execution with separation logic [berdine:aplas:2005]
Implicit dynamic frames: Combining dynamic frames and separation logic [smans:ecoop:2009]
Lightweight support for magic wands in an automatic verifier [schwerhoff:ecoop:2015]
Software verification with VeriFast: Industrial case studies [philippaerts:scp:2014]
Viper: A verification infrastructure for permission-based reasoning [muller:vmcai:2016]
Leveraging Rust types for modular specification and verification [astrauskas:oopsla:2019]
VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
seL4: from general purpose to a proof of information flow enforcement [murray:secpriv:2013]
Permission accounting in separation logic [bornat:popl:2005]
Separation logic [ohearn:cacm:2019]
Separation logic: a logic for shared mutable data structures [reynolds:lics:2002]
A solver for reachability modulo theories [lal:cav:2012]
Sound formal verification of Linux's USB BP keyboard driver [penninckx:nfm:2012]
VeriFast: Imperative programs as proofs [jacobs:vstte:2010]
Annotation inference for separation logic based verifiers [vogels:fmoods:2011]
Stacked borrows: An aliasing model for Rust [jung:popl:2020]
The case for writing a kernel in Rust [levy:apsys:2017]
Verifying Rust programs with SMACK [baranowski:atva:2018]
Crust: A bounded verifier for Rust [toman:ase:2015]
A type system for expressive security policies [walker:popl:2000]
RustBelt: Securing the foundations of the Rust programming language [jung:popl:2017]
Alias types [smith:esop:2000]
TALx86: A realistic typed assembly language [morrisett:wcsss:1999]
End-to-end verification of information flow security for C and assembly programs [costanzo:pldi:2016]
A precise yet efficient memory model for C [cohen:entcs:2009]
Frama-C: A software analysis perspective [cuoq:sefm:2012]
CertiKOS: An extensible architecture for building certified concurrent OS Kernels [gu:osdi:2016]
Formal verification of a memory allocation module of Contiki with Frama-C: a case study [mangano:crisis:2016]
überSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor [vasudevan:usenix:2016]
Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor [becker:fm:2016]
-Overify: Optimizing programs for fast verification [wagner:hotos:2013]
A lightweight symbolic virtual machine for solver-aided host languages [torlak:pldi:2014]
An abstract interpretation framework for refactoring with application to extract methods with contracts [cousot:oopsla:2012]
Komodo: Using verification to disentangle secure-enclave hardware from software [ferraiuolo:sosp:2017]
Attacking, repairing, and verifying SecVisor: A retrospective on the security of a hypervisor [franklin:cmu:2008]
SecVisor: A tiny hypervisor to provide lifetime kernel code integrity for commodity OSes [seshadri:sosp:2007]
Verifying security invariants in ExpressOS [mai:asplos:2013]
Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
The existence of refinement mappings [abadi:tcs:1991]
SpaceSearch: A library for building and verifying solver-aided tools [weitz:icfp:2017]
Boost the impact of continuous formal verification in industry [monteiro:arxiv:2019]
Multi-prover verification of C programs [filliatre:fem:2004]
Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
Scalable translation validation of unverified legacy OS code [tahat:fmcad:2019]
Noninterference, transitivity, and channel-control security policies [rushby:sri:1992]
Secure information flow by self composition [barthe:csfw:2004]
SMACK: Decoupling source language details from verifier implementations [rakamaric:cav:2014]
Local verification of global invariants in concurrent programs [cohen:cav:2010]
A hardware design language for timing-sensitive information flow security [zhang:asplos:2015]
Complete information flow tracking from the gates up [tiwari:asplos:2009]
The Flask security architecture: System support for diverse security policies [spencer:security:1999]
On the foundations of quantitative information flow [smith:fossacs:2009]
Theoretical analysis of gate level information flow tracking [oberg:dac:2010]
Secure autonomous cyber-physical systems through verifiable information flow control [liu:cpsspc:2018]
Verifying the Microsoft Hyper-V hypervisor with VCC [leinenbach:fm:2009]
SecChisel: Language and tool for practical and scalable security verification of security-aware hardware architectures [deng:hasp:2019]
Verifying constant-time implementations [almeida:security:2016]
Interposition agents: transparently interposing user code at the system interface [jones:sosp:1993]
Units: Cool modules for HOT languages [flatt:pldi:1998]
A structured TCP in Standard ML [biagioni:sigcomm:1994]
The Flux OSKit: A substrate for kernel and language research [ford:sosp:1997]

Backlog of papers to summarize

Souper: A Synthesizing Superoptimizer [sasnauskas:arxiv:2018]
Solving Exists/Forall Problems With Yices [dutertre:smt:2015]
Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts [wang:sigsac:2023]
Security Verification via Automatic Hardware-Aware Exploit Synthesis: The CheckMate Approach [trippel:micro:2019]
Full-Stack Memory Model Verification with TriCheck [trippel:micro:2018]
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA [trippel:asplos:2017]
Directed Proof Generation for Machine Code [thakur:cav:2010]
Revizor: testing black-box CPUs against speculation contracts [oleksenko:asplos:2022]
Valgrind: A Program Supervision Framework [nethercote:rv:2003]
Swivel: Hardening WebAssembly against Spectre [narayan:sec:2021]
Axiomatic hardware-software contracts for security [mosier:isca:2022]
Spectre Attacks: Exploiting Speculative Execution [kocher:sandp:2019]
Jakstab: A Static Analysis Platform for Binaries [kinder:cav:2008]
The Gates of Time: Improving Cache Attacks with Transient Execution [katzman:sec:2023]
Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model Implementations [hsiao:micro:2021]
Static Analysis of Memory Models for SMT Encodings [haas:oopsla:2023]
Automatic Detection of Speculative Execution Combinations [fabian:ccs:2022]
Computing with time: microarchitectural weird machines [evtyushkin:asplos:2021]
Weird Machines, Exploitability, and Provable Unexploitability [dullien:tetc:2020]
SoK: Practical Foundations for Software Spectre Defenses [cauligi:sandp:2022]
Constant-time foundations for the new spectre era [cauligi:pldi:2020]
On Subnormal Floating Point and Abnormal Timing [andrysco:sandp:2015]
A Comprehensive Survey on the Non-Invasive Passive Side-Channel Analysis [socha:sensors:2022]
Covering all the bases: Type-based verification of test input generators [zhou:pldi:2023]
Synthesizing MILP constraints for efficient and robust optimization [wang:pldi:2023]
Obtaining information leakage bounds via approximate model counting [saha:pldi:2023]
Fuzzing loop optimizations in compilers for C++ and data-parallel languages [livinskii:pldi:2023]
VMSL: A separation logic for mechanised robust safety of virtual machines communicating above FF-A [liu:pldi:2023]
CryptOpt: Verified compilation with randomized program search for cryptographic primitives [kuepper:pldi:2023]
Indexed streams: A formal intermediate representation for fused contraction programs [kovach:pldi:2023]
Don't look UB: Exposing sanitizer-eliding compiler optimizations [isemann:pldi:2023]
Absynthe: Abstract interpretation-guided synthesis [guria:pldi:2023]
CommCSL: Proving information flow security for concurrent programs using abstract commutativity [eilers:pldi:2023]
An automata-based framework for verification and bug hunting in quantum circuits [chen:pldi:2023]
Better defunctionalization through lambda set specialization [brandon:pldi:2023]
Mosaic: An interoperable compiler for tensor algebra [bansal:pldi:2023]
Efficient parallel functional programming with effects [arora:pldi:2023]
Modular hardware design with timeline types [rachit:pldi:2023]
Modular Hardware Design with Timeline Types [nigam:pldi:2023]
Noninterference specifications for secure systems [nelson:osr:2020]
Better together: Unifying datalog and equality saturation [zhang:pldi:2023]
egg: Fast and extensible equality saturation [willsey:popl:2021]
Rewrite rule inference using equality saturation [willsey:oopsla:2021]
Vectorization for digital signal processors via equality saturation [vanhattum:asplos:2021]
Equality saturation: A new approach to optimization [tate:popl:2009]
Pure tensor program rewriting via access patterns (representation pearl) [smith:maps:2021]
Synthesizing structured CAD models with equality saturation and inverse transformations [nandi:pldi:2020]
Small proofs from congruence closure [flatt:fmcad:2022]
Microkernels meet recursive virtual machines [ford:sosp:1996]
A2: Analog malicious hardware [yang:sandp:2016]
GSTE is partitioned model checking [sebastiani:cav:2004]
Flip Feng Shui: Hammering a needle in the software stack [razavi:usenix:2016]
UCLID5: Multi-modal formal modeling, verification, and synthesis [polgreen:cav:2022]
RTLcheck: Verifying the memory consistency of RTL designs [manerkar:micro:2017]
SoK: Design tools for side-channel-aware implementations [buhan:ccs:2022]
Revisiting capacitor-based Trojan design [bidmeshki:iccd:2019]
Stealthy dopant-level hardware Trojans [becker:ches:2013]
ZSim: Fast and accurate microarchitectural simulation of thousand-core systems [sanchez:isca:2013]
Zsim: A fast architectural simulator for ISA design-space exploration [lifshitz:wish:2011]
Specification of Intel IA-32 using an architecture description language [bastian:adl:2005]
Raising binaries to LLVM IR with MCTOLL (WIP paper) [yadavalli:lctes:2019]
BitBlaze: A new approach to computer security via binary analysis [song:iciss:2008]
The New Jersey machine-code toolkit [ramsey:usenix:1995]
N-version disassembly: Differential testing of x86 disassemblers [paleari:issta:2010]
Pin: Building customized program analysis tools with dynamic instrumentation [luk:pldi:2005]
Reverse-engineering instruction encodings [hsieh:usenix:2001]
Lifting assembly to intermediate representation: A novel approach leveraging compilers [hasabnis:asplos:2016]
Rev.Ng: A unified binary analysis framework to recover CFGs and function boundaries [difederico:cc:2017]
Reverse interpretation + mutation analysis = automatic retargeting [collberg:pldi:1997]
An in-depth analysis of disassembly on full-scale x86/x64 binaries [andriesse:usenix:2016]
A compiler-level intermediate representation based binary analysis and rewriting system [anand:eurosys:2013]
BinRec: Dynamic binary lifting and recompilation [altinay:eurosys:2020]
Verified just-in-time compiler on x86 [myreen:popl:2010]
A verified runtime for a verified theorem prover [myreen:itp:2011]
Hoare logic for ARM machine code [myreen:fse:2007]
Dataflow-based pruning for speeding up superoptimization [mukherjee:oopsla:2020]
Randomised testing of a microprocessor model using SMT-solver state generation [campbell:fmics:2014]
Dependent ML An approach to practical programming with dependent types [xi:jfp:2007]
CHERI: A hybrid capability-system architecture for scalable software compartmentalization [watson:sandp:2015]
Formal verification of a multiprocessor hypervisor on Arm relaxed memory hardware [tao:sosp:2021]
A new verified compiler backend for CakeML [tan:icfp:2016]
Program verification in the presence of cached address translation [syeda:itp:2018]
ARMv8-A system semantics: Instruction fetch in relaxed architectures [simner:pls:2020]
x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors [sewell:cacm:2010]
CompCertTSO: A verified compiler for relaxed-memory concurrency [sevcik:jacm:2013]
Liquid types [rondon:pldi:2008]
Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8 [pulte:popl:2017]
Valgrind: A framework for heavyweight dynamic binary instrumentation [nethercote:pldi:2007]
Lem: Reusable engineering of real-world semantics [mulligan:icfp:2014]
TSL: A system for generating abstract interpreters and its application to machine-code analysis [lim:toplas:2013]
Formally verified memory protection for a commodity multiprocessor hypervisor [li:usenix:2021]
Coq: The world's best macro assembler? [kennedy:ppdp:2013]
Towards verified faithful simulation [joloboff:dsetta:2015]
High-level separation logic for low-level code [jensen:popl:2013]
Verified compilation of CakeML to multiple machine-code targets [fox:cpp:2017]
Mixed-size concurrency: ARM, POWER, C/C++11, and SC [flur:popl:2017]
Automatically generating instruction selectors using declarative machine descriptions [dias:popl:2010]
Extracting behaviour from an executable instruction set model [campbell:fmcad:2016]
BAP: A binary analysis platform [brumley:cav:2011]
A high assurance virtualization platform for ARMv8 [baumann:eucnc:2016]
Isla: Integrating full-scale ISA semantics and axiomatic concurrency models [armstrong:cav:2021]
Certified complexity (CerCo) [amadio:fpara:2014]
Automatic generation and validation of instruction encoders and decoders [xu:cav:2021]
Design of a symbolically executable embedded hypervisor [nordholz:eurosys:2020]
Proving LTL properties of bitvector programs and decompiled binaries (extended) [liu:arxiv:2021]
Towards verified binary raising [hendrix:itp:2019]
Verifying x86 instruction implementations [goel:cpp:2020]
Balancing automation and control for formal verification of microprocessors [goel:cav:2021]
Scalable validation of binary lifters [dasgupta:pldi:2020]
Formal verification of pipelined Y86-64 microprocessors with UCLID5 [bryant:cmu:2018]
Vale: Verifying high-performance cryptographic assembly code [bond:usenix:2017]
Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the sockets API [bishop:jacm:2019]
Rigging the lottery: Making all tickets winners [evci:arxiv:2021]
Motivation for and evaluation of the first tensor processing unit [jouppi:micro:2018]
TimeWarp: Rethinking timekeeping and performance monitoring mechanisms to mitigate side-channel attacks [martin:isca:2012]
Product programs in the wild: Retrofitting program verifiers to check information flow security [marco:cav:2021]
The tail at scale [dean:cacm:2013]
Verified security for the Morello capability-enhanced prototype Arm architecture [bauereiss:ucam:2021]
The dogged pursuit of bug-free C programs: The Frama-C software analysis platform [baudin:cacm:2021]
Integration verification across software and hardware for a simple embedded system [erbsen:pldi:2021]
The role of formalism in system requirements [bruel:compsurv:2021]
Demystifying attestation in Intel Trust Domain Extensions via formal verification [sardar:access:2021]
Evaluating large language models trained on code [chen:arxiv:2021]
Modular specification and verification of closures in Rust (draft paper) [wolff:draft:2021]
Static automated program repair for heap properties [vantonder:icse:2018]
Uncovering the hidden dangers: Finding unsafe Go code in the wild [lauinger:trustcom:2020]
Complete type inference for simple objects [wand:lics:1987]
A safe interface to sockets [reppy:att:1996]
Type checking records and variants in a natural extension of ML [remy:popl:1989]
Faking it: Simulating dependent types in Haskell [mcbride:jfp:2002]
Calling hell from heaven and heaven from hell [finne:icfp:1999]
Type extension through polymorphism [burton:toplas:1990]
No-longer-foreign: Teaching an ML compiler to speak C "natively" [blume:babel:2001]
Reticle: A virtual machine for programming modern FPGAs [vega:pldi:2021]
RefinedC: Automating the foundational verification of C code with refined ownership types [sammler:pldi:2021]
Beyond the elementary representations of program invariants over algebraic data types [kostyukov:pldi:2021]
K-induction without unrolling [gurfinkel:fmcad:2017]
How do committees invent [conway:datamation:1968]
Editor's note: How to write research articles in computing and engineering disciplines [stojmenovic:tpds:2010]
FuzzFactory: Domain-specific fuzzing with waypoints [padhye:oopsla:2019]
Semantic fuzzing with Zest [padhye:issta:2019]
Alive2: Bounded translation validation for LLVM [lopes:pldi:2021]
Why don't software developers use static analysis tools to find bugs? [johnson:icse:2013]
Examiner: Automatically locating inconsistent instructions between real devices and CPU emulators for Arm [jiang:arxiv:2021]
Efficient sampling of SAT solutions for testing [dutra:icse:2018]
The Rust language [matsakis:hilt:2014]
Ownership types for flexible alias protection [clarke:oopsla:1998]
You can't spell trust without Rust [beingessner:msc:2015]
Towards optimization-safe systems: Analyzing the impact of undefined behavior [wang:sosp:2013]
SoK: Eternal war in memory [szekeres:sandp:2013]
Send hardest problems my way: Probabilistic path prioritization for hybrid fuzzing [zhao:ndss:2019]
Memoized symbolic execution [yang:issta:2012]
Relocatable addressing model for symbolic execution [trabish:issta:2020]
Checking safety properties using induction and a SAT-solver [sheeran:fmcad:2000]
Zero-overhead path prediction with progressive symbolic execution [rutledge:icse:2019]
Bug synthesis: Challenging bug-finding tools with deep faults [roy:fse:2018]
Hybrid concolic testing [majumdar:icse:2007]
Just fuzz it: Solving floating-point constraints using coverage-Guided fuzzing [liew:fse:2019]
A secure and formally verified Linux KVM hypervisor [li:sandp:2021]
On symbolic execution of decompiled programs [korencik:qrs:2020]
Automated behavioral regression testing [jin:icst:2010]
Micro execution [godefroid:icse:2014]
Program state abstraction for feedback-driven fuzz testing using likely invariants [fioraldi:arxiv:2020]
Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level [daniel:sandp:2020]
Coz: Finding code that counts with causal profiling [curtsinger:cacm:2018]
Inception: System-wide security testing of real-world embedded systems software [corteggiani:usenix:2018]
Symbiotic 8: Beyond symbolic execution [chalupa:tacas:2021]
Running symbolic execution forever [busse:issta:2020]
Countermeasures optimization in multiple fault-injection context [boespflug:fdtc:2020]
Model checking of C and C++ with DIVINE 4 [baranova:atva:2017]
Systematic comparison of symbolic execution systems: Intermediate representation and its generation [poeplau:acsac:2019]
EXE: Automatically Generating Inputs of Death [cadar:tiss:2008]
Accurate, efficient, and adaptive calling context profiling [zhuang:pldi:2006]
Symbolic partial-order execution for testing multi-threaded programs [schemmel:cav:2020]
Get rid of inline assembly through verification-oriented lifting [recoules:ase:2019]
Learning-based memory allocation for C++ server workloads [maas:asplos:2020]
BHive: A benchmark suite and measurement framework for validating x86-64 basic block performance models [chen:iiswc:2019]
Compositional may-must program analysis: Unleashing the power of alternation [godefroid:popl:2010]
Scaling static analyses at Facebook [distefano:cacm:2019]
Incorrectness logic [ohearn:popl:2019]
Verifying software network functions with no verification expertise [zaostrovnykh:sosp:2019]
Symbolic execution of multithreaded programs from arbitrary program contexts [bergan:oopsla:2014]
Finding and understanding bugs in C compilers [yang:pldi:2011]
CUTE: A concolic unit testing engine for C [sen:fse:2005]
Differential symbolic execution [person:fse:2008]
Sys: A static/symbolic tool for finding good bugs in good (browser) code [brown:sec:2020]
How to build static checking systems using orders of magnitude less code [brown:asplos:2016]
p4v: Practical verification for programmable data planes [liu:sigcomm:2018]
Shape analysis for composite data structures [berdine:cav:2007]
Verifying systems rules using rule-directed symbolic execution [cui:asplos:2013]
Execution levels for aspect-oriented programming [tanter:aosd:2010]
Interoperability-guided testing of QUIC implementations using symbolic execution [rath:epiq:2018]
No crash, no exploit: Automated verification of embedded kernels [nicole:arxiv:2020]
InSpectre: Breaking and fixing microarchitectural vulnerabilities by formal analysis [guanciale:ccs:2020]
Specification of concretization and symbolization policies in symbolic execution [david:issta:2016]
SymNav: Visually assisting symbolic execution [angelini:vizsec:2019]
Symbolic memory with pointers [trtik:atva:2014]
Unleashing Mayhem on binary code [cha:sandp:2012]
Formulog: Datalog for SMT-based static analysis [bembenek:oopsla:2020]
Region-based memory management [tofte:inco:1997]
Exploiting mixed binaries [papaevripides:acmtps:2021]
Region-based memory management in Cyclone [grossman:pldi:2002]
Fidelius Charm: Isolating unsafe Rust code [almohri:codaspy:2018]
Formal methods for privacy [tschantz:fm:2009]
Mutation testing advances: An analysis and survey (chapter 6) [papadakis:advances:2019]
An analysis and survey of the development of mutation testing [jia:ieeetse:2010]
VRLifeTime - An IDE tool to avoid concurrency and memory bugs in Rust [zhang:ccs:2020]
Memory-safety challenge considered solved? An in-depth study with all Rust CVEs [xu:arxiv:2021]
Securing unsafe Rust programs with XRust [liu:icse:2020]
Automatic heap layout manipulation for exploitation [heelan:sec:2018]
Automatic generation of control flow hijacking exploits for software vulnerabilities [heelan:msc:2009]
Extended support for borrowing and lifetimes in Prusti [gorse:msc:2020]
Deductive program verification for a language with a Rust-like typing discipline type [Internship report] [denis:hal:2020]
Verifying safe clients of unsafe code and trait implementations in Rust [beckmann:msc:2020]
The Axiom profiler: Understanding and debugging SMT quantifier instantiations [becker:tacas:2019]
Automatic exploit generation [avgerinos:cacm:2014]
Learning Rust: How experienced programmers leverage resources to learn a new programming language [abtahi:chi:2020]
Towards making formal methods normal: meeting developers where they are [reid:hatra:2020]
Towards practical reactive security audit using extended static checkers [vanegue:sandp:2013]
PG-KLEE: Trading soundness for coverage [rutledge:icse:2020]
Methods for binary symbolic execution [romano:phd:2014]
Deferred concretization in symbolic execution via fuzzing [pandey:issta:2019]
Noninterference via symbolic execution [milushev:forte:2012]
Symbolic execution with existential second-order constraints [mechtaev:fse:2018]
Control flow obfuscation using neural network to fight concolic testing [ma:securecomm:2015]
Boost symbolic execution using dynamic state merging and forking [zhang:apsec:2018]
Using test ranges to improve symbolic execution [qiu:nfm:2018]
Targeted program transformations for symbolic execution [cadar:fse:2015]
Specification: The biggest bottleneck in formal methods and autonomy [rozier:vstte:2016]
Hackers vs. testers: A comparison of software vulnerability discovery processes [votipka:sp:2018]
Programmers are users too: Human-centered methods for improving programming tools [myers:computer:2016]
PLIERS: A process that integrates user-centered methods into programming language design [coblenz:arxiv:2020]
Gradual program verification [bader:vmcai:2018]
LLVM: a compilation framework for lifelong program analysis and transformation [lattner:cgo:2004]
Theseus: A state spill-free operating system [boos:plos:2017]
SHErrLoc: A static holistic error locator [zhang:toplas:2017]
The tip of the iceberg: On the merits of finding security bugs [alexopoulos:tps:2020]
BP: Formal proofs, the fine print and side effects [murray:secdev:2018]
Code coverage at Google [ivankovic:fse:2019]
Testability of software components [freedman:tse:1991]
The effect of certain modular design principles on testability [edwards:icrs:1975]
Design for testability in object-oriented systems [binder:cacm:1994]
Bigtable: A distributed storage system for structured data [chang:tocs:2012]
On the origin of objects [smith:book:1996]
Moving from the design of usable security technologies to the design of useful secure applications [smetters:nspw:2002]
Usability evaluation with the cognitive walkthrough [rieman:chi:1995]
Cognitive dimensions of information artefacts: a tutorial [green:tutorial:1998]
Cognitive dimensions of notations [green:pandc:1990]
A static analyzer for finding dynamic programming errors [bush:spe:2000]
Using test case reduction and prioritization to improve symbolic execution [zhang:issta:2014]
Specifying representations of machine instructions [ramsey:toplas:1997]
Machine descriptions to build tools for embedded systems [ramsey:lctes:1998]
Automatic checking of instruction specifications [fernandez:icse:1997]
UQBT: Adaptable binary translation at low cost [cifuentes:computer:2000]
Formal verification by symbolic evaluation of partially-ordered trajectories [segar:fmsd:1995]
An introduction to symbolic trajectory evaluation [claessen:sfm:2006]
A survey of computer hardware description languages in the U.S.A. [su:computer:1974]
A PMS level notation for the description and simulation of digital systems [djordjevic:cj:1985]
Simulation of a horizontal bit-sliced processor using the ISPS architecture simulation facility [dam:ieeetc:1981]
Three decades of HDLs: Part I, CDL through TI-HDL [chu:ieeedtc:1992]
Automated exploration of the design space for register transfer (RT) systems [barbacci:isca:1973]
Instruction set processor specifications (ISPS): The notation and its applications [barbacci:ieeetc:1981]
A comparison of register transfer languages for describing computers and digital systems [barbacci:ieeetc:1975]
Programming at the Processor-Memory-Switch level [barbacci:icse:1988]
Instruction set processor specifications for simulation, evaluation, and synthesis [barbacci:dac:1979]
Using emulation to verify formal architecture descriptions [barbacci:computer:1978]
Evaluation of the CFA test programs via formal computer descriptions [barbacci:computer:1977]
PMS: A notation to describe computer structures [barbacci:computer:1973]
An architectural research facility: ISP descriptions, simulation, data collection [barbacci:afips:1977]
ISP: A notation to describe a computer's instruction sets [barbacci2:computer:1973]
Superoptimizer: A look at the smallest program [massalin:asplos:1987]
Computer structures: Readings and examples [bell:book:1971]
Design and programming of embedded multiprocessors: An interface-centric approach [wolf:codes:2004]
Polymorphic type inference for machine code [noonan:pldi:2016]
Single-ISA heterogeneous multi-core architectures for multithreaded workload performance [kumar:isca:2004]
Denali: A goal-directed superoptimizer [joshi:pldi:2002]
Evaluating general purpose automated theorem proving systems [sutcliffe:ai:2001]
Test-case reduction for C compiler bugs [regehr:pldi:2012]
One test to rule them all [groce:issta:2017]
LSCs: Breathing life into message sequence charts [damm:fmoods:1999]
The temporal logic of programs [pnueli:sfcs:1977]
Driller: Augmenting fuzzing through selective symbolic execution [stephens:ndss:2016]
SoK: (state of) the art of war: Offensive techniques in binary analysis [shoshitaishvili:sp:2016]
All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask) [schwartz:sp:2010]
DART: Directed automated random testing [godefroid:pldi:2005]
The S2E platform: Design, implementation, and applications [chipounov:tcs:2012]
S2E: A platform for in-vivo multi-path analysis of software systems [chipounov:asplos:2011]
Deconstructing dynamic symbolic execution [ball:dsse:2015]
SMT proof checking using a logical framework [stump:fmsd:2013]
Detecting critical bugs in SMT solvers using blackbox mutational fuzzing [mansur:arxiv:2020]
Automated testing and debugging of SAT and QBF solvers [brummayer:sat:2010]
Proofs in satisfiability modulo theories [barrett:mlf:2015]
The CHERI capability model: Revisiting RISC in an age of risk [woodruff:isca:2014]
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process [nienhuis:secpriv:2020]
CIL: Intermediate language and tools for analysis and transformation of C programs [necula:cc:2002]
The Rust programming language [klabnik:book:2018]
Software verification with BLAST [henzinger:spin:2003]
The BLAST query language for software verification [beyer:sas:2004]
The software model checker BLAST: Applications to software engineering [beyer:ijsttt:2007]
CPAchecker: A tool for configurable software verification [beyer:cav:2011]
Automatic predicate abstraction of C programs [ball:pldi:2001]
A tool for checking ANSI-C programs [clarke:tacas:2004]
Counterexample-guided abstraction refinement [clarke:cav:2000]
Proof-carrying code [necula:popl:1997]
Reasoning about comprehensions with first-order SMT solvers [leino:sac:2009]
Dynamic frames: Support for framing, dependencies and sharing without restrictions [kassios:fm:2006]
Witnessing the elimination of magic wands [blom:ijsttt:2015]
Behavioral interface specification languages [hatcliff:compsurv:2012]
The Spec# programming system: Challenges and directions [barnett:vstte:2005]
A reachability predicate for analyzing low-level software [chatterjee:tacas:2007]
Assertion-based encapsulation, object invariants and simulations [naumann:fmco:2004]
Rust distilled: An expressive tower of languages [weiss:arxiv:2018]
Heap-dependent expressions in separation logic [smans:fmood:2010]
Type-based decompilation (or program reconstruction via type reconstruction) [mycroft:esop:1999]
Abstract read permissions: Fractional permissions without the fractions [heule:vmcai:2013]
CIVL: the concurrency intermediate verification language [siegel:sc:2015]
SeL4: Formal verification of an OS kernel [klein:sosp:2009]
Views: Compositional reasoning for concurrent programs [dinsdale-young:popl:2013]
A semantics for concurrent separation logic [brookes:tcs:2006]
Resources, concurrency, and local reasoning [ohearn:tcs:2007]
Specifying concurrent programs in separation logic: Morphisms and simulations [nanevski:oopsla:2019]
Ynot: Dependent types for imperative programs [nanevski:icfp:2008]
Existential types for imperative languages [grossman:esop:2002]
Multiprogramming a 64kB computer safely and efficiently [levy:sosp:2017]
Ownership is theft: Experiences building an embedded OS in Rust [levy:plos:2015]
KRust: A formal executable semantics of Rust [wang:tase:2018]
LLBMC: Bounded model checking of C and C++ programs using a compiler IR [merz:vstte:2012]
The SeaHorn verification framework [gurfinkel:cav:2015]
System programming in Rust: Beyond safety [balasubramanium:hotos:2017]
Cogent: Verifying high-assurance file system implementations [amani:asplos:2016]
A dependently typed assembly language [xi:icfp:2001]
Alias types for recursive data structures [walker:tic:2001]
Enforcing high-level protocols in low-level software [deline:pldi:2001]
CSeq: a concurrency pre-processor for sequential C verification tools [fischer:ase:2013]
Model checking boot code from AWS data centers [cook:cav:2018]
Automated verification of a small hypervisor [alkassar:vstte:2010]
A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C [blanchard:fmics:2015]
Verification of TLB virtualization implemented in C [alkassar:vstte:2012]
Design, implementation and verification of an extensible and modular hypervisor framework [vasudevan:secpriv:2013]
Growing solver-aided languages with Rosette [torlak:onward:2013]
A polymorphic intermediate verification language: Design and logical encoding [leino:tacas:2010]
Testing noninterference, quickly [hritcu:icfp:2013]
Static contract checking with abstract interpretation [fahndrich:foveoos:2010]
Locking discipline inference and checking [ernst:icse:2016]
Reliable and fast DWARF-based stack unwinding [bastian:oopsla:2019]
Large-scale formal verification in practice: A process perspective [andronick:icse:2012]
Virtualization: Issues, security threats, and solutions [pearce:compsurv:2013]
Implementing an untrusted operating system on trusted hardware [lie:sosp:2003]
Specifying and verifying hardware for tamper-resistant software [lie:secpri:2003]
Safe to the last instruction: automated verification of a type-safe operating system [yang:pldi:2010]
Practical verification for the working programmer with CodeContracts and abstract interpretation [logozzo:vmcai:2011]
Applying source-code verification to a microkernel: the VFiasco project [hohmuth:sigops:2002]
The VFiasco approach for a verified operating system [hohmuth:plos:2005]
A framework for cooperating decision procedures [barrett:cade:2000]
The Lean theorem prover (system description) [demoura:cade:2015]
Machine code verification of a tiny ARM hypervisor [dam:trusted:2013]
The Spec# programming system: An overview [barnett:cassis:2004]
Establishing a refinement relation between binaries and abstract code [verbeek:fmmsd:2019]
Push-button verification of file systems via crash refinement [sigurbjarnarson:osdi:2016]
Hyperkernel: Push-button verification of an OS kernel [nelson:sosp:2017]
RedLeaf: Towards an operating system for safe and verified firmware [narayanan:hotos:2019]
Verified compilation on a verified processor [loow:pldi:2019]
Powering the static driver verifier using Corral [lal:fse:2014]
Machine assisted proof of ARMv7 instruction level isolation properties [khakpour:cpp:2013]
Ironclad apps: End-to-end security via automated full-system verification [hawblitzel:osdi:2014]
Why3 — where programs meet provers [filliatre:esop:2013]
The Why/Krakatoa/Caduceus platform for deductive program verification [filliatre:cav:2007]
Secure information flow verification with mutable dependent types [ferraiuolo:dac:2017]
Verification of a practical hardware security architecture through static information flow analysis [ferraiuolo:asplos:2017]
Z3: An efficient SMT solver [demoura:tacas:2008]
Unifying type checking and property checking for low-level code [condit:popl:2009]
The last mile: An empirical study of timing channels on seL4 [cock:ccs:2014]
Making information flow explicit in HiStar [zeldovich:osdi:2006]
Observational determinism for concurrent program security [zdancewic:csfw:2003]
Robust declassification [zdancewic:csfw:2001]
Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security [tiwari:isca:2011]
Execution leases: A hardware-supported mechanism for enforcing strong non-interference [tiwari:isca:2009]
Nickel: A framework for design and verification of information flow control systems [sigurbjarnarson:osdi:2018]
Declassification: Dimensions and principles [sabelfield:jcs:2009]
Enforcing robust declassification [myers:csfw:2004]
Preserving information flow properties under refinement [mantel:sp:2001]
Controlling the what and where of declassification in language-based security [mantel:pls:2007]
Information flow control for standard OS abstractions [krohn:sosp:2007]
Unwinding and inference control [goguen:secpriv:1984]
Security policies and security models [goguen:secpriv:1982]
HyperFlow: A processor architecture for nonmalleable, timing-safe information flow security [ferraiuolo:ccs:2018]
Labels and event processes in the Asbestos operating system [efstathopoulos:sosp:2005]
A lattice model of secure information flow [denning:cacm:1976]
Hyperproperties [clarkson:jcs:2010]
Provably secure compilation of side-channel countermeasures. [barthe:iacr:2007]
LISA – machine description language and generic machine model for HW/SW co-design [zivojnovic:vlsi:1996]
Integrating memory consistency models with instruction-level abstraction for heterogeneous system-on-chip verification [zhang:fmcad:2018]
Formal modeling and verification of microprocessors [windley:ieeetoc:1995]
Automatically comparing memory consistency models [wickerson:popl:2017]
EXOCHI: architecture and programming environment for a heterogeneous multi-core multithreaded system [wang:pldi:2007]
Continuation-based multiprocessing [wand:lfp:1980]
Why events are a bad idea (for high-concurrency servers) [vonbehren:hotos:2003]
Formal verification of superscalar microprocessors with multicycle functional units, exception, and branch prediction [velev:dac:2000]
Active libraries: Rethinking the roles of compilers and libraries [veldhuizen:oo:1998]
VIS speeds new media processing [tremblay:micro:1996]
Teleport messaging for distributed stream programs [thies:ppopp:2005]
A practical approach to exploiting coarse-grained pipeline parallelism in C programs [thies:micro:2007]
CLKSCREW: Exposing the perils of security-oblivious energy management [tang:sec:2017]
IEEE standard for SystemVerilog - Unified hardware design, specification, and verification language [systemverilog:ieee:2013]
Exploiting task and data parallelism on a multicomputer [subhlok:ppopp:1993]
Processor memory system verification using DOGReL: a language for specifying end-to-end properties [stewart:difts:2014]
Decoupled access/execute computer architectures [smith:tocs:1984]
A flexible formal verification framework for industrial scale validation [slobodova:memocode:2011]
A comparative study of SYCL, OpenCL, and OpenMP [silva:sbac:2016]
ARM Architecture Reference Manual (ARMv5 edition) [seal:book:2000]
Automatic derivation of platform noninterference properties [schwarz:sefm:2016]
Integrated semantics of intermediate-language C and macro-assembler for pervasive formal verification of operating systems and hypervisors from VerisoftXT [schmaltz:vstte:2012]
A machine description facility for compiler testing [samet:ieeetse:1977]
The CRAY-1 computer system [russell:cacm:1978]
Formally verified big step semantics out of x86-64 binaries [roessle:cpp:2019]
Software foundations [pierce:book:2016]
MMX technology extension to the Intel architecture [peleg:micro:1996]
PDP-11/45 processor handbook [pdp11:book:1973]
The case for the reduced instruction set computer [patterson:sigarch:1980]
Reduced instruction set computers [patterson:cacm:1985]
Decoupling integer execution in superscalar processors [palacharla:micro:1995]
Why threads are a bad idea (for most purposes) (Invited talk) [ousterhout:usenix:1996]
Abstractions from tests [naik:popl:2012]
Processor description languages [mishra:book:2008]
A theory of type polymorphism in programming [milner:jcss:1978]
Verification of an implementation of Tomasulo's algorithm by compositional model checking [mcmillan:cav:1998]
Spectre is here to stay: An analysis of side-channels and speculative execution [mcilroy:arxiv:2019]
Easy approach to requirements syntax (EARS) [mavin:isre:2009]
Vx86: x86 assembler simulated in C powered by automated theorem proving [maus:amast:2008]
Quantifying information flow [lowe:csfw:2015]
Meltdown [lipp:arxiv:2018]
Memory coherence in shared virtual memory systems [li:tocs:1989]
Subword parallelism with MAX-2 [lee:micro:1996]
On the duality of operating system structures [lauer:osr:1979]
DAG inlining: A decision procedure for reachability-modulo-theories in hierarchical programs [lal:pldi:2015]
Automated formal verification of processors based on architectural models [kuhne:fmcad:2010]
Proving the correctness of pipelined micro-architectures [kroening:itg:2000]
Automated pipeline design [kroening:dac:2001]
Scalable vector media processors for embedded systems [kozyrakis:phd:2002]
Differential power analysis [kocher:crypto:1999]
Spectre attacks: Exploiting speculative execution [kocher:arxiv:2018]
Symbolic trajectory evaluation: The primary validation vehicle for next generation Intel processor graphics FPU [kirankumar:fmcad:2012]
Flipping bits in memory without accessing them: An experimental study of DRAM disturbance errors [kim:isca:2014]
Towards a new model of abstraction in software engineering [kiczales:iwoos:1991]
An industrial strength theorem prover for a logic based on Common Lisp [kaufmann:ieeetse:1997]
Replacing testing with formal verification in Intel Core i7 processor execution engine validation [kaivola:cav:2009]
Playing by the rules: rewriting as a practical optimisation technique in GHC [jones:microsoft:2001]
CRL: High-performance all-software distributed shared memory [johnson:osr:1995]
Microarchitecture verification by compositional model checking [jhala:cav:2001]
Alloy: A lightweight object modelling notation [jackson:tosem:2002]
Verifying the FM9801 microarchitecture [hunt:micro:1999]
Microprocessor design verification [hunt:jar:1989]
Computer architecture: A quantitative approach (Fifth edition) [hennessy:book:2011]
An annotation language for optimizing software libraries [guyer:dsl:1999]
A retrospective on `MIPS: A microprocessor architecture' [gross:micro:2016]
Introduction to HOL: A Theorem Proving Environment for Higher Order Logic [gordon:book:1993]
A stream compiler for communication-exposed architectures [gordon:asplos:2002]
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware [ge:jce:2016]
The nesC language: A holistic approach to networked embedded systems [gay:pldi:2003]
Model checking early requirements specifications in Tropos [fuxman:isre:2001]
DynAlloy: Upgrading Alloy with Actions [frias:icse:2005]
Formal verification of the ARM6 micro-architecture [fox:ucam:2002]
Very high-speed computing systems [flynn:ieeeproc:1966]
Very long instruction word architectures and the ELI-512 [fisher:isca:1983]
Describing instruction set processors using nML [fauth:edtc:1995]
Protothreads: Simplifying Event-driven Programming of Memory-constrained Embedded Systems [dunkels:enss:2006]
Compiler support for exploiting coarse-grained pipelined parallelism. [du:sc:2003]
Using continuations to implement thread management and communication in operating systems [draves:sosp:1991]
Automatically partitioning packet processing applications for pipelined architectures [dai:pldi:2005]
Event-driven programming for robust software [dabek:sigops:2002]
Constructions: A higher order proof system for mechanizing mathematics [coquand:eurocal:1985]
Design of a separable transition-diagram compiler [conway:cacm:1963]
Design and synthesis of synchronization skeletons using branching-time temporal logic [clarke:wlop:1982]
Quantitative analysis of the leakage of confidential data [clark:entcs:2002]
Specifying the semantics of machine instructions [cifuentes:iwpc:1998]
Translating formal software specifications to natural language / A grammar-based approach [burke:lacl:2005]
Revisiting the sequential programming model for multi-core [bridges:micro:2007]
Experience with embedding hardware description languages in HOL [boulton:tpcd:1993]
A trusted mechanised JavaScript specification [bodin:popl:2014]
Vector models for data-parallel computing [blelloch:book:1990]
Implementing remote procedure calls [birrell:tocs:1984]
The effectiveness of decoupling [bird:sc:1993]
An approach to systems verification [bevier:jar:1989]
The Midway distributed shared memory system [bershad:cmpcon:1993]
Hardware is the new software [baumann:hotos:2017]
Secure information flow by self-composition [barthe:mscs:2011]
CVC4 [barrett:cav:2011]
Vector microprocessors [asanovic:phd:1998]
A survey of asynchronous remote procedure calls [ananda:osr:1992]
A methodology for large-scale hardware verification [aagaard:fmcad:2000]
Solver aided reverse engineering of architectural features [zorn:iscawddd:2017]
Automatic refinement checking of pipelines with out-of-order execution [srinivasan:ieeetoc:2010]
Certification of an instruction set simulator [shi:phd:2013]
A data driven approach for algebraic loop invariants [sharma:pls:2013]
Data-driven equivalence checking [sharma:oopsla:2012]
Translation validation for a verified OS kernel [sewell:pldi:2013]
The semantics of x86-CC multiprocessor machine code [sarkar:popl:2009]
Understanding POWER multiprocessors [sarkar:pldi:2011]
Automatically proving the correctness of translations involving optimized code. [samet:phd:1975]
Deriving abstract transfer functions for analyzing embedded software [regehr:lctes:2006]
Translation validation [pnueli:tacas:1998]
Isabelle/HOL: A proof assistant for higher-order logic [nipkow:book:2002]
Boolector 2.0 [niemetz:jsat:2015]
Translation validation for an optimizing compiler [necula:pldi:2000]
Verified LISP Implementations on ARM, x86 and PowerPC [myreen:tphols:2009]
Functional programs: Conversions between deep and shallow embeddings [myreen:itp:2012]
RockSalt: Better, faster, stronger SFI for the x86 [morrisett:pldi:2012]
Path-exploration lifting: Hi-fi tests for lo-fi emulators [martignoni:asplos:2012]
COATCheck: Verifying memory ordering at the hardware-OS interface [lustig:asplos:2016]
Provably correct peephole optimizations with Alive [lopes:pldi:2015]
Pydgin: generating fast instruction set simulators from simple architecture descriptions with meta-tracing JIT compilers [lockhart:ispass:2015]
Formal verification of a realistic compiler [leroy:cacm:2009]
Experience with term level modeling and verification of the M* CORE microprocessor core [lahiri:hldvt:2001]
Deductive verification of advanced out-of-order microprocessors [lahiri:cav:2003]
CakeML: A verified implementation of ML [kumar:popl:2014]
Towards a formal model of the x86 ISA [kaufmann:utaustin:2012]
FM8501: A verified microprocessor [hunt:lncs:1994]
Instruction-level abstraction (ILA): A uniform specification for system-on-chip (SoC) verification [huang:todaes:2019]
Simplifying design and verification for structural hazards and datapaths in pipelined circuits [higgins:hldvt:2004]
Stratified synthesis: Automatically learning the x86-64 instruction set [heule:pldi:2016]
MIPS: A microprocessor architecture [hennessy:micro:1982]
A robust machine code proof framework for highly secure applications [hardin:acl2:2006]
Symbolic simulation of the JEM1 microprocessor [greve:fmcad:1998]
An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors [gray:micro:2015]
Formal verification of application and system programs based on a validated x86 ISA model [goel:phd:2016]
Engineering a formal, executable x86 ISA simulator for software verification [goel:pcs:2017]
Simulation and formal verification of x86 machine-code programs that make system calls [goel:fmcad:2014]
Abstract stobjs and their application to ISA modeling [goel:acl2:2013]
Automated synthesis of symbolic instruction encodings from I/O samples [godefroid:pldi:2012]
SAGE: Whitebox fuzzing for security testing [godefroid:acmq:2012]
A knowledge-based code generator generator [fraser:sigart:1977]
Formal specification and verification of ARM6 [fox:tphols:2003]
Improved tool support for machine-code decompilation in HOL4 [fox:itps:2015]
Directions in ISA specification [fox:itp:2012]
A trustworthy monadic formalization of the ARMv7 instruction set architecture [fox:itp:2010]
A HOL specification of the ARM instruction set architecture [fox:cambridge:2001]
An empirical study on the correctness of formally verified distributed systems [fonseca:ecs:2017]
Modelling the ARMv8 architecture, operationally: concurrency and ISA [flur:popl:2016]
A formal description of SYSTEM/360 [falkoff:ibm:1964]
Formal specification of the x86 instruction set architecture [degenbaev:phd:2012]
A complete formal semantics of x86-64 user-level instruction set architecture [dasgupta:pldi:2019]
Machine code verification of a tiny ARM hypervisor [dam:ted:2013]
Reasoning about the ARM weakly consistent memory model [chong:asplos:2008]
Automatic derivation of code generators from machine descriptions [cattell:toplas:1980]
Formalization and automatic derivation of code generators [cattell:phd:1978]
KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs [cadar:osdi:2008]
Automatic verification of pipelined microprocessor control [burch:cav:1994]
Designing a CPU model: from a pseudo-formal document to fast code [blanqui:rapido:2011]
Symbolic model checking without BDDs [biere:tacas:1999]
Putting it all together - Formal verification of the VAMP [beyer:ijsttt:2006]
The PMS and ISP descriptive systems for computer structures [bell:afips:1970]
The Satisfiability Modulo Theories Library (SMT-LIB) [barrett:smtlib:2016]
The oracle problem in software testing: A survey [barr:tse:2015]
Instruction set processor specifications (ISPS): The notation and its applications [barbacci:ieee:1981]
ISP: A language to describe instruction sets and other register transfer systems [barbacci:cmu:1972]
Binary translation using peephole superoptimizers [bansal:osdi:2008]
Automatic generation of peephole superoptimizers [bansal:asplos:2006]
Herding cats: Modelling, simulation, testing, and data mining for weak memory [alglave:toplas:2014]
Testing the FM9001 microprocessor [albin:cli:1995]
A framework for microprocessor correctness statements [aagaard:charme:2001]
From SODA to scotch: The evolution of a wireless baseband processor [woh:micro:2008]
The ARM scalable vector extension [stephens:micro:2017]
The Hugs graphics library (version 2.0) [reid:yale:2001]
Designing the standard Haskell libraries [reid:yale:1998]
Defining interfaces between hardware and software: Quality and performance [reid:phd:2019]
Knit: Component composition for systems software [reid:osdi:2000]
Who guards the guards? Formal validation of the ARM v8-M architecture specification [reid:oopsla:2017]
A precise semantics for ultraloose specifications [reid:msc:1993]
Putting the spine back in the Spineless Tagless G-Machine: An implementation of resumable black-holes [reid:ifl:1998]
Prototyping real-time vision systems: An experiment in DSL design [reid:icse:1999]
A proposal for the standard Haskell libraries [reid:hw:1995]
Malloc pointers and stable pointers: Improving Haskell's foreign language interface [reid:gfpw:1994]
Implementing Fudgets with standard widget sets [reid:gfpw:1993]
Designing data structures [reid:gfpw:1989]
Trustworthy specifications of ARM v8-A and v8-M system level architecture [reid:fmcad:2016]
End-to-end verification of ARM processors with ISA-formal [reid:cav:2016]
SoC-C: efficient programming abstractions for heterogeneous multicore systems on chip [reid:cases:2008]
Eliminating stack overflow by abstract interpretation [regehr:tecs:2005]
Evolving real-time systems using hierarchical scheduling and concurrency analysis [regehr:rtss:2003]
Eliminating stack overflow by abstract interpretation [regehr:emsoft:2003]
HOIST: a system for automatically deriving static analyzers for embedded systems [regehr:asplos:2004]
Lock inference for systems software [regehr:acp4is:2003]
FVision: A declarative language for visual tracking [peterson:padl:2001]
Adding records to Haskell [peterson:hw:1995]
Low-cost techniques for reducing branch context pollution in a soft realtime embedded multithreaded processor [ozer:sbacpad:2007]
Design and implementation of turbo decoders for software defined radio [lin:sips:2006]
SPEX: A programming language for software defined radio [lin:sdr:2006]
A semantics for imprecise exceptions [jones:pldi:1999]
Green Card: a foreign-language interface for Haskell [jones:hw:1997]
Standard libraries for the Haskell 98 programming language [jones:hasklib:1999]
Haskell 98: A non-strict, purely functional language [jones:hasklang:1999]
Using x86isa for microcode verification [goel:spisa:2019]
Static and dynamic structure in design patterns [eide:icse:2002]
Aspect weaving as component knitting: Separating concerns with Knit [eide:aspse:2001]
The Haskell 98 foreign function interface 1.0: An addendum to the Haskell 98 report [chakravarty:haskffi:2003]
Advanced SIMD: Extending the reach of contemporary SIMD architectures [boettcher:date:2014]
The state of Sail [armstrong:spisa:2019]
ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS [armstrong:popl19:2019]
Detailed models of instruction set architectures: From pseudocode to formal semantics [armstrong:arw:2018]
Rudra: Finding memory safety bugs in Rust at the Ecosystem scale [rudra:sosp:2021]