| Layered and Object-Based Game Semantics | 0 | 0.34 | 2022 |
| Adore: Atomic Distributed Objects with Certified Reconfiguration | 0 | 0.34 | 2022 |
| TimeDice: Schedulability-Preserving Priority Inversion for Mitigating Covert Timing Channels Between Real-time Partitions | 0 | 0.34 | 2022 |
| CompCertO: compiling certified open C components | 0 | 0.34 | 2021 |
| Blinder: Partition-Oblivious Hierarchical Scheduling | 0 | 0.34 | 2021 |
| Paired Training Framework for Time-Constrained Learning. | 0 | 0.34 | 2021 |
| Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems | 0 | 0.34 | 2021 |
| Adaptive Generative Modeling in Resource-Constrained Environments | 0 | 0.34 | 2021 |
| Refinement-Based Game Semantics for Certified Abstraction Layers | 0 | 0.34 | 2020 |
| Task-Aware Novelty Detection for Visual-based Deep Learning in Autonomous Systems. | 0 | 0.34 | 2020 |
| Novelty Detection via Network Saliency in Visual-Based Deep Learning | 0 | 0.34 | 2019 |
| Integrating Formal Schedulability Analysis Into A Verified Os Kernel | 1 | 0.36 | 2019 |
| An abstract stack based approach to verified compositional compilation to machine code. | 0 | 0.34 | 2019 |
| Building certified concurrent OS kernels | 1 | 0.36 | 2019 |
| A new hierarchical software architecture towards safety-critical aspects of a drone system | 1 | 0.36 | 2019 |
| Toward compositional verification of interruptible OS kernels and device drivers. | 5 | 0.44 | 2018 |
| End-to-end verification of information-flow security for C and assembly programs. | 8 | 0.46 | 2016 |
| Compositional certified resource bounds | 29 | 0.79 | 2015 |
| Automatic Static Cost Analysis for Parallel Programs | 14 | 0.61 | 2015 |
| Clean-Slate Development of Certified OS Kernels | 1 | 0.36 | 2015 |
| A Compositional Semantics for Verified Separate Compilation and Linking | 4 | 0.44 | 2015 |
| Deep Specifications and Certified Abstraction Layers | 12 | 0.57 | 2015 |
| Compositional verification of termination-preserving refinement of concurrent programs | 13 | 0.64 | 2014 |
| Type-Based Amortized Resource Analysis with Integers and Arrays. | 8 | 0.46 | 2014 |
| End-to-end verification of stack-space bounds for C programs | 5 | 0.45 | 2014 |
| A Separation Logic for Enforcing Declarative Information Flow Control Policies. | 3 | 0.39 | 2014 |
| Trace-Based Temporal Verification for Message-Passing Programs | 0 | 0.34 | 2014 |
| Characterizing progress properties of concurrent objects via contextual refinements | 10 | 0.53 | 2013 |
| Quantitative Reasoning for Proving Lock-Freedom | 13 | 0.58 | 2013 |
| Proving the correctness of concurrent robot software | 1 | 0.44 | 2012 |
| Compositional verification of a baby virtual memory manager | 7 | 0.50 | 2012 |
| A Case for Behavior-Preserving Actions in Separation Logic. | 2 | 0.39 | 2012 |
| Modular Verification of Concurrent Thread Management. | 5 | 0.42 | 2012 |
| Static and user-extensible proof checking | 7 | 0.53 | 2012 |
| A structural approach to prophecy variables | 3 | 0.38 | 2012 |
| A Simple Model for Certifying Assembly Programs with First-Class Function Pointers | 2 | 0.38 | 2011 |
| Weak Updates and Separation Logic | 2 | 0.40 | 2011 |
| Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings | 28 | 1.78 | 2011 |
| CertiKOS: a certified kernel for secure cloud computing | 21 | 0.82 | 2011 |
| VeriML: typed computation of logical terms inside a language with effects | 11 | 0.63 | 2010 |
| Reasoning about optimistic concurrency using a program logic for history | 24 | 0.86 | 2010 |
| Certified software | 6 | 0.46 | 2010 |
| Parameterized memory models and concurrent separation logic | 15 | 0.72 | 2010 |
| Modular Development of Certified System Software | 0 | 0.34 | 2009 |
| Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009 | 6 | 0.72 | 2009 |
| Certifying low-level programs with hardware interrupts and preemptive threads | 52 | 2.26 | 2008 |
| Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems | 14 | 0.80 | 2008 |
| Using XCAP to certify realistic systems code: machine context management | 32 | 3.52 | 2007 |
| A general framework for certifying garbage collectors and their mutators | 38 | 1.64 | 2007 |
| On the relationship between concurrent separation logic and assume-guarantee reasoning | 58 | 2.53 | 2007 |
