|
|
|
|
Venues (Conferences, Journals, ...)
|
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 31 occurrences of 18 keywords
|
|
|
|
|
Results
Found 18 publication records. Showing 18 according to the selection in the facets
| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Adam Chlipala |
Mostly-automated verification of low-level programs in computational separation logic.  |
PLDI  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Chlipala |
Ur: statically-typed metaprogramming with type-level record computation. |
PLDI |
2010 |
DBLP DOI BibTeX RDF |
dependent types, metaprogramming |
| 1 | Adam Chlipala |
Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. |
OSDI |
2010 |
DBLP BibTeX RDF |
|
| 1 | Adam Chlipala |
A verified compiler for an impure functional language. |
POPL |
2010 |
DBLP DOI BibTeX RDF |
compiler verification, interactive proof assistants |
| 1 | Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky |
Effective interactive proofs for higher-order imperative programs. |
ICFP |
2009 |
DBLP DOI BibTeX RDF |
functional programming, dependent types, separation logic, interactive proof assistants |
| 1 | Adam Chlipala |
Modular development of certified program verifiers with a proof assistant, . |
J. Funct. Program. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Chlipala |
Parametric higher-order abstract syntax for mechanized semantics. |
ICFP |
2008 |
DBLP DOI BibTeX RDF |
type-theoretic semantics, dependent types, compiler verification, interactive proof assistants |
| 1 | Adam Chlipala |
Position Paper: Thoughts on Programming with Proof Assistants. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Chlipala |
A certified type-preserving compiler from lambda calculus to assembly language. |
PLDI |
2007 |
DBLP DOI BibTeX RDF |
denotational semantics, dependent types, compiler verification, interactive proof assistants |
| 1 | Adam Chlipala |
Modular development of certified program verifiers with a proof assistant. |
ICFP |
2006 |
DBLP DOI BibTeX RDF |
programming with dependent types, proof-carrying code, interactive proof assistants |
| 1 | Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula |
A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. |
VMCAI |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Chlipala, Leaf Petersen, Robert Harper |
Strict bidirectional type checking. |
TLDI |
2005 |
DBLP DOI BibTeX RDF |
strict logic, type inference, type theory |
| 1 | Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck |
The open verifier framework for foundational verifiers. |
TLDI |
2005 |
DBLP DOI BibTeX RDF |
language-based security, proof-carrying code, typed assembly language |
| 1 | Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck |
Type-based verification of assembly language for compiler debugging. |
TLDI |
2005 |
DBLP DOI BibTeX RDF |
abstract interpretation, dependent types, bytecode verification, certified compilation, assembly code |
| 1 | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
Invited talk: the blast query language for software verification. |
PEPM |
2004 |
DBLP DOI BibTeX RDF |
software verification, software specification |
| 1 | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
Invited talk: the blast query language for software verification. |
PPDP |
2004 |
DBLP DOI BibTeX RDF |
software verification, software specification |
| 1 | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
The Blast Query Language for Software Verification.. |
SAS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
Generating Tests from Counterexamples. |
ICSE |
2004 |
DBLP DOI BibTeX RDF |
|
Displaying result #1 - #18 of 18 (100 per page; Change: )
|
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")