Zhong Shao

Jung-Eun Kim

Richard M. Bradford

Proceedings of the 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2022

2021

Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Blinder: Partition-Oblivious Hierarchical Scheduling.

[BibT_eX]

[DOI]

Proceedings of the 30th USENIX Security Symposium, 2021

CompCertO: compiling certified open C components.

[BibT_eX]

[DOI]

Jérémie Koenig

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Paired Training Framework for Time-Constrained Learning.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2021

Adaptive Generative Modeling in Resource-Constrained Environments.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2021

2020

CompCertELF: verified separate compilation of C programs into ELF object files.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Refinement-Based Game Semantics for Certified Abstraction Layers.

[BibT_eX]

[DOI]

Jérémie Koenig

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Task-Aware Novelty Detection for Visual-based Deep Learning in Autonomous Systems.

[BibT_eX]

[DOI]

Valerie Chen

Proceedings of the 2020 IEEE International Conference on Robotics and Automation, 2020

ABC: Abstract prediction Before Concreteness.

[BibT_eX]

[DOI]

Proceedings of the 2020 Design, Automation & Test in Europe Conference & Exhibition, 2020

AnytimeNet: Controlling Time-Quality Tradeoffs in Deep Neural Network Architectures.

[BibT_eX]

[DOI]

Jung-Eun Kim

Richard M. Bradford

Proceedings of the 2020 Design, Automation & Test in Europe Conference & Exhibition, 2020

2019

An abstract stack based approach to verified compositional compilation to machine code.

[BibT_eX]

[DOI]

Yuting Wang

Pierre Wilke

Proc. ACM Program. Lang., 2019

DeepSEA: a language for certified system software.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

A new hierarchical software architecture towards safety-critical aspects of a drone system.

[BibT_eX]

[DOI]

Frontiers Inf. Technol. Electron. Eng., 2019

TaskShuffler++: Real-Time Schedule Randomization for Reducing Worst-Case Vulnerability to Timing Inference Attacks.

[BibT_eX]

[DOI]

CoRR, 2019

Building certified concurrent OS kernels.

[BibT_eX]

[DOI]

Commun. ACM, 2019

ADLP: Accountable Data Logging Protocol for Publish-Subscribe Communication Systems.

[BibT_eX]

[DOI]

Proceedings of the 39th IEEE International Conference on Distributed Computing Systems, 2019

Novelty Detection via Network Saliency in Visual-Based Deep Learning.

[BibT_eX]

[DOI]

Valerie Chen

Proceedings of the 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops, 2019

WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems.

[BibT_eX]

[DOI]

Srihari Radhakrishnan

Mahesh Balakrishnan

Proceedings of the ACM Symposium on Cloud Computing, SoCC 2019, 2019

Integrating Formal Schedulability Analysis into a Verified OS Kernel.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers.

[BibT_eX]

[DOI]

J. Autom. Reason., 2018

Certified concurrent abstraction layers.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

2017

Automated Resource Analysis with Coq Proof Objects.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Safety and Liveness of MCS Lock - Layer by Layer.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2016

End-to-end verification of information-flow security for C and assembly programs.

[BibT_eX]

[DOI]

David Costanzo

Ronghui Gu

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.

[BibT_eX]

[DOI]

Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, 2016

2015

Type-based amortized resource analysis with integers and arrays.

[BibT_eX]

[DOI]

J. Funct. Program., 2015

Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2015

Deep Specifications and Certified Abstraction Layers.

[BibT_eX]

[DOI]

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Compositional certified resource bounds.

[BibT_eX]

[DOI]

Quentin Carbonneaux

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Automatic Static Cost Analysis for Parallel Programs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2015

Clean-Slate Development of Certified OS Kernels.

[BibT_eX]

[DOI]

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

A Compositional Semantics for Verified Separate Compilation and Linking.

[BibT_eX]

[DOI]

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

Trace-Based Temporal Verification for Message-Passing Programs.

[BibT_eX]

[DOI]

Jinjiang Lei

Zongyan Qiu

Proceedings of the 2014 Theoretical Aspects of Software Engineering Conference, 2014

A Separation Logic for Enforcing Declarative Information Flow Control Policies.

[BibT_eX]

[DOI]

David Costanzo

Proceedings of the Principles of Security and Trust - Third International Conference, 2014

End-to-end verification of stack-space bounds for C programs.

[BibT_eX]

[DOI]

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

Compositional verification of termination-preserving refinement of concurrent programs.

[BibT_eX]

[DOI]

Hongjin Liang

Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013

Quantitative Reasoning for Proving Lock-Freedom.

[BibT_eX]

[DOI]

Michael Marmar

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Characterizing Progress Properties of Concurrent Objects via Contextual Refinements.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

2012

A Structural Approach to Prophecy Variables.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Models of Computation, 2012

Static and user-extensible proof checking.

[BibT_eX]

[DOI]

Antonis Stampoulis

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Proving the correctness of concurrent robot software.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Conference on Robotics and Automation, 2012

Compositional Verification of a Baby Virtual Memory Manager.

[BibT_eX]

[DOI]

Alexander Vaynberg

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

Modular Verification of Concurrent Thread Management.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

A Case for Behavior-Preserving Actions in Separation Logic.

[BibT_eX]

[DOI]

David Costanzo

Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011

Weak Updates and Separation Logic.

[BibT_eX]

[DOI]

New Gener. Comput., 2011

A Simple Model for Certifying Assembly Programs with First-Class Function Pointers.

[BibT_eX]

[DOI]

Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011

CertiKOS: a certified kernel for secure cloud computing.

[BibT_eX]

[DOI]

Proceedings of the APSys '11 Asia Pacific Workshop on Systems, 2011

2010

Certified software.

[BibT_eX]

[DOI]

Commun. ACM, 2010

VeriML: typed computation of logical terms inside a language with effects.

[BibT_eX]

[DOI]

Antonis Stampoulis

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

Parameterized Memory Models and Concurrent Separation Logic.

[BibT_eX]

[DOI]

Rodrigo Ferreira

Proceedings of the Programming Languages and Systems, 2010

Reasoning about Optimistic Concurrency Using a Program Logic for History.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

2009

Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads.

[BibT_eX]

[DOI]

J. Autom. Reason., 2009

Modular Development of Certified System Software.

[BibT_eX]

[DOI]

Proceedings of the TASE 2009, 2009

2008

Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2008

2007

Using XCAP to Certify Realistic Systems Code: Machine Context Management.

[BibT_eX]

[DOI]

Zhaozhong Ni

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

An open framework for foundational proof-carrying code.

[BibT_eX]

[DOI]

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

Foundational Typed Assembly Language with Certified Garbage Collection.

[BibT_eX]

[DOI]

Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

A general framework for certifying garbage collectors and their mutators.

[BibT_eX]

[DOI]

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

Certified self-modifying code.

[BibT_eX]

[DOI]

Hongxu Cai

Alexander Vaynberg

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

On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning.

[BibT_eX]

[DOI]

Rodrigo Ferreira

Proceedings of the Programming Languages and Systems, 2007

2006

Certified assembly programming with embedded code pointers.

[BibT_eX]

[DOI]

Zhaozhong Ni

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

Modular verification of assembly code with stack-based control abstractions.

[BibT_eX]

[DOI]

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

2005

A type system for certified binaries.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2005

Modular verification of concurrent assembly code with dynamic thread creation and termination.

[BibT_eX]

[DOI]

Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

2004

Building certified libraries for PCC: dynamic storage allocation.

[BibT_eX]

[DOI]

Nadeem Abdul Hamid

Sci. Comput. Program., 2004

Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code.

[BibT_eX]

[DOI]

Nadeem Abdul Hamid

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Verification of safety properties for concurrent assembly code.

[BibT_eX]

[DOI]

Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, 2004

2003

Intensional analysis of quantified types.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2003

Inlining as staged computation.

[BibT_eX]

[DOI]

Stefan Monnier

J. Funct. Program., 2003

A Syntactic Approach to Foundational Proof-Carrying Code.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

Precision in Practice: A Type-Preserving Java Compiler.

[BibT_eX]

[DOI]

Proceedings of the Compiler Construction, 12th International Conference, 2003

2002

Type-preserving compilation of Featherweight Java.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2002

Supporting Binary Compatibility with Static Compilation.

[BibT_eX]

[DOI]

Proceedings of the 2nd Java Virtual Machine Research and Technology Symposium, 2002

2001

Invited Talk: Towards a Principled Multi-Language Infrastructure.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Multi-Language Infrastructure and Interoperability, 2001

Principled Scavenging.

[BibT_eX]

[DOI]

Stefan Monnier

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

2000

Efficient and safe-for-space closure conversion.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2000

Typed common intermediate format.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 2000

Fully reflexive intensional type analysis.

[BibT_eX]

[DOI]

Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), 2000

1999

Transparent Modules with Fully Syntactic Signatures.

[BibT_eX]

[DOI]

Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

Representing Java Classes in a Typed Intermediate Language.

[BibT_eX]

[DOI]

Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

Safe and Principled Language Interoperation.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 1999

1998

Type-Directed Continuation Allocation.

[BibT_eX]

[DOI]

Proceedings of the Types in Compilation, Second International Workshop, 1998

Optimal Type Lifting.

[BibT_eX]

[DOI]

Proceedings of the Types in Compilation, Second International Workshop, 1998

Implementing Typed Intermediate Languages.

[BibT_eX]

[DOI]

Stefan Monnier

Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), 1998

Typed Cross-Module Compilation.

[BibT_eX]

[DOI]

Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), 1998

1997

Flexible Representation Analysis.

[BibT_eX]

[DOI]

Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997

1996

Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures.

[BibT_eX]

[DOI]

J. Funct. Program., 1996

1995

A Type-Based Compiler for Standard ML.

[BibT_eX]

[DOI]

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

1994

Unrolling Lists.

[BibT_eX]

[DOI]

John H. Reppy

Proceedings of the 1994 ACM Conference on LISP and Functional Programming, 1994

Space-Efficient Closure Representations.

[BibT_eX]

[DOI]

Proceedings of the 1994 ACM Conference on LISP and Functional Programming, 1994

1993

Smartest Recompilation.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

1992

Callee-Save Registers in Continuation-Passing Style.

[BibT_eX]