George C. Necula

Koushik Sen

Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Towards hinted collection: annotations for decreasing garbage collector pause times.

[BibT_eX]

[DOI]

Philip Reames

Proceedings of the International Symposium on Memory Management, 2013

2012

CCured: type-safe retrofitting of legacy code.

[BibT_eX]

[DOI]

Scott McPeak

ACM SIGPLAN Notices, 2012

A model and framework for reliable build systems

[BibT_eX]

[DOI]

Derrick Coetzee

Anand Bhaskar

CoRR, 2012

NDetermin: inferring nondeterministic sequential specifications for parallelism correctness.

[BibT_eX]

[DOI]

Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2012

CONCURRIT: Testing Concurrent Programs with Programmable State-Space Exploration.

[BibT_eX]

[DOI]

Proceedings of the 4th USENIX Workshop on Hot Topics in Parallelism, 2012

2011

Proof-Carrying Code.

[BibT_eX]

[DOI]

Proceedings of the Encyclopedia of Cryptography and Security, 2nd Ed., 2011

NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness.

[BibT_eX]

[DOI]

Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

Specifying and checking semantic atomicity for multithreaded programs.

[BibT_eX]

[DOI]

Jacob Burnim

Koushik Sen

Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, 2011

2008

Exceptional situations and program reliability.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2008

2007

Enforcing resource bounds via static verification of dynamic checks.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2007

A polynomial-time algorithm for global value numbering.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2007

Shape Analysis with Structural Invariant Checkers.

[BibT_eX]

[DOI]

Bor-Yuh Evan Chang

Xavier Rival

Proceedings of the Static Analysis, 14th International Symposium, 2007

Beyond Bug-Finding: Sound Program Analysis for Linux.

[BibT_eX]

[DOI]

Proceedings of HotOS'07: 11th Workshop on Hot Topics in Operating Systems, 2007

Dependent Types for Low-Level Programming.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2007

2006

Preface.

[BibT_eX]

[DOI]

Jens Knoop

Wolf Zimmermann

Proceedings of the 5th International Workshop on Compiler Optimization meets Compiler Verification, 2006

A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety.

[BibT_eX]

[DOI]

Bor-Yuh Evan Chang

Adam Chlipala

Proceedings of the Verification, 2006

Analysis of Low-Level Code Using Cooperating Decompilers.

[BibT_eX]

[DOI]

Bor-Yuh Evan Chang

Matthew Harren

Proceedings of the Static Analysis, 13th International Symposium, 2006

SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques.

[BibT_eX]

[DOI]

Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI '06), 2006

XFI: Software Guards for System Address Spaces.

[BibT_eX]

[DOI]

Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI '06), 2006

Using Dependent Types to Port Type Systems to Low-Level Languages.

[BibT_eX]

[DOI]

Proceedings of the Compiler Construction, 15th International Conference, 2006

2005

CCured: type-safe retrofitting of legacy software.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2005

A randomized satisfiability procedure for arithmetic and uninterpreted function symbols.

[BibT_eX]

[DOI]

Inf. Comput., 2005

Type-based verification of assembly language for compiler debugging.

[BibT_eX]

[DOI]

Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

The open verifier framework for foundational verifiers.

[BibT_eX]

[DOI]

Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

Mining Temporal Specifications for Error Detection.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Using Dependent Types to Certify the Safety of Assembly Code.

[BibT_eX]

[DOI]

Matthew Harren

Proceedings of the Static Analysis, 12th International Symposium, 2005

Precise interprocedural analysis using random interpretation.

[BibT_eX]

[DOI]

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Data Slicing: Separating the Heap into Independent Regions.

[BibT_eX]

[DOI]

Jeremy Condit

Proceedings of the Compiler Construction, 14th International Conference, 2005

Randomized Algorithms for Program Analysis and Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Data Structure Specifications via Local Equality Axioms.

[BibT_eX]

[DOI]

Scott McPeak

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

JVer: A Java Verifier.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 11th International Symposium, 2004

Global value numbering using random interpretation.

[BibT_eX]

[DOI]

Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

Finding and preventing run-time error handling mistakes.

[BibT_eX]

[DOI]

Proceedings of the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2004

Join Algorithms for the Theory of Uninterpreted Functions.

[BibT_eX]

[DOI]

Ashish Tiwari

Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

By Reason and Authority: A System for Authorization of Proof-Carrying Code.

[BibT_eX]

[DOI]

Nathan Whitehead

Martín Abadi

Proceedings of the 17th IEEE Computer Security Foundations Workshop, 2004

Elkhound: A Fast, Practical GLR Parser Generator.

[BibT_eX]

[DOI]

Scott McPeak

Proceedings of the Compiler Construction, 13th International Conference, 2004

2003

Capriccio: scalable threads for internet services.

[BibT_eX]

[DOI]

Proceedings of the 19th ACM Symposium on Operating Systems Principles 2003, 2003

Discovering affine equalities using random interpretation.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

CCured in the real world.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, 2003

A Sound Framework for Untrusted Verification-Condition Generators.

[BibT_eX]

[DOI]

Robert R. Schneck

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Lightweight Wrappers for Interfacing with Binary Code in CCured.

[BibT_eX]

[DOI]

Matthew Harren

Proceedings of the Software Security, 2003

A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

Proof-Carrying Code with Untrusted Proof Rules.

[BibT_eX]

[DOI]

Robert R. Schneck

Proceedings of the Software Security -- Theories and Systems, 2002

CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs.

[BibT_eX]

[DOI]

Proceedings of the Compiler Construction, 11th International Conference, 2002

Temporal-Safety Proofs for Systems Code.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code.

[BibT_eX]

[DOI]

Robert R. Schneck

Proceedings of the Automated Deduction, 2002

2001

Oracle-based checking of untrusted software.

[BibT_eX]

[DOI]

Shree Prakash Rahul

Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001

A Scalable Architecture for Proof-Carrying Code.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 5th International Symposium, 2001

2000

A logic-based approach to software system safety and security.

[BibT_eX]

[DOI]

Shree Prakash Rahul

ACM SIGSOFT Softw. Eng. Notes, 2000

Proof-carrying code: design, implementation and applications (abstract).

[BibT_eX]

[DOI]

Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, 2000

Translation validation for an optimizing compiler.

[BibT_eX]

[DOI]

Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2000

A certifying compiler for Java.

[BibT_eX]

[DOI]

Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2000

A Proof-Carrying Code Architecture for Java.

[BibT_eX]

[DOI]

Christopher Colby

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Proof Generation in the Touchstone Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2000

1999

Enforcing Security and Safety with Proof-Carrying Code.

[BibT_eX]

[DOI]

Proceedings of the Fifteenth Conference on Mathematical Foundations of Progamming Semantics, 1999

1998

The design and implementation of a certifying compiler (with retrospective)

[BibT_eX]

[DOI]

Proceedings of the 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, 1998

The Design and Implementation of a Certifying Compiler.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN '98 Conference on Programming Language Design and Implementation (PLDI), 1998

Safe, Untrusted Agents Using Proof-Carrying Code.

[BibT_eX]

[DOI]

Proceedings of the Mobile Agents and Security, 1998

Efficient Representation and Validation of Proofs.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

1997

Research on Proof-Carrying Code for Untrusted-Code Security.

[BibT_eX]

[DOI]

Proceedings of the 1997 IEEE Symposium on Security and Privacy, 1997

Proof-Carrying Code.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997

1996

Safe Kernel Extensions Without Run-Time Checking.

[BibT_eX]

[DOI]