Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
11 | Ming Fu, Yu Zhang 0086, Yong Li |
Formal Reasoning about Concurrent Assembly Code with Reentrant Locks. |
TASE |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Sylvie Boldo, Guillaume Melquiond |
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. |
IEEE Trans. Computers |
2008 |
DBLP DOI BibTeX RDF |
Verification, Computer arithmetic |
11 | Marc Bezem, Dimitri Hendriks |
On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic. |
J. Autom. Reason. |
2008 |
DBLP DOI BibTeX RDF |
Coherent logic, Proof objects, Hessenberg’s theorem, Automated theorem proving |
11 | Ulrich Schöpp |
A Formalised Lower Bound on Undirected Graph Reachability. |
LPAR |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca |
Canonical Big Operators. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Matthieu Sozeau, Nicolas Oury |
First-Class Type Classes. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks 0001, Iulian Neamtiu |
Formalizing Soundness of Contextual Effects. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Mike Gordon |
Twenty Years of Theorem Proving for HOLs Past, Present and Future. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Ralph Matthes |
Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening. |
MPC |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Noam Zeilberger |
Focusing and higher-order abstract syntax. |
POPL |
2008 |
DBLP DOI BibTeX RDF |
pattern-matching, higher-order abstract syntax, focusing |
11 | Bruno Barras, Bruno Bernardo |
The Implicit Calculus of Constructions as a Programming Language with Dependent Types. |
FoSSaCS |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli |
Oracle Semantics for Concurrent Separation Logic. |
ESOP |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Juan Manuel Crespo, Gustavo Betarte, Carlos Luna 0001 |
A Framework for the Analysis of Access Control Models for Interactive Mobile Devices. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
mobile devices, Access control models, formal proofs |
11 | Erik Ernst |
First-Class Object Sets. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
Object sets, multi-object method calls, composition, types |
11 | Cezary Kaliszyk, Freek Wiedijk |
Merging Procedural and Declarative Proof. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Laura Effinger-Dean, Matthew Kehrt, Dan Grossman |
Transactional events for ML. |
ICFP |
2008 |
DBLP DOI BibTeX RDF |
synchronous message passing, transactional events, concurrency |
11 | Guillaume Melquiond |
Proving Bounds on Real-Valued Functions with Computations. |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Rawle C. S. Prince, Neil Ghani, Conor McBride |
Proving Properties about Lists Using Containers. |
FLOPS |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Nicolas Julien |
Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base. |
FLOPS |
2008 |
DBLP DOI BibTeX RDF |
|
11 | David Nowak |
On Formal Verification of Arithmetic-Based Cryptographic Primitives. |
ICISC |
2008 |
DBLP DOI BibTeX RDF |
machine formalization, CSPRBG, semantic security, cryptographic primitives |
11 | Paulo F. Silva 0001, José Nuno Oliveira |
'Galculator': functional prototype of a Galois-connection based proof assistant. |
PPDP |
2008 |
DBLP DOI BibTeX RDF |
point-free notation, haskell, DSL, Galois connections, proof assistant, GADT |
11 | Laurent Hubert, Thomas P. Jensen, David Pichardie |
Semantic Foundations and Inference of Non-null Annotations. |
FMOODS |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Adam Koprowski, Johannes Waldmann |
Arctic Termination ...Below Zero. |
RTA |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub |
From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures. |
IFIP TCS |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Adam Koprowski, Hans Zantema |
Certification of Proving Termination of Term Rewriting by Matrix Interpretations. |
SOFSEM |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Frédéric Gava, Jean Fortin |
Formal Semantics of a Subset of the Paderborn's BSPlib. |
PDCAT |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Chunxiao Lin, Yiyun Chen, Long Li, Bei Hua |
Garbage Collector Verification for Proof-Carrying Code. |
J. Comput. Sci. Technol. |
2007 |
DBLP DOI BibTeX RDF |
program safety, program verification, proof-carrying code, garbage collector |
11 | Alberto Ciaffaglione, Luigi Liquori, Marino Miculan |
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. |
J. Autom. Reason. |
2007 |
DBLP DOI BibTeX RDF |
Functional and imperative object-calculi, Logical foundations of programming, Coinductive type theories, Logical frameworks, Interactive theorem proving |
11 | Bart Jacobs 0001, Sjaak Smetsers, Ronny Wichers Schreur |
Code-carrying theories. |
Formal Aspects Comput. |
2007 |
DBLP DOI BibTeX RDF |
Compression, Code generation, Functional languages, Unification, PVS, Proof assistants |
11 | Benjamin Grégoire, Jorge Luis Sacchini |
Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. |
TGC |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Éric Jaeger, Catherine Dubois |
Why Would You Trust B ? |
LPAR |
2007 |
DBLP DOI BibTeX RDF |
Prover, Deep embedding, Formal Methods, Confidence |
11 | Zaynah Dargaye, Xavier Leroy |
Mechanized Verification of CPS Transformations. |
LPAR |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Seth Fogarty, Emir Pasalic, Jeremy G. Siek, Walid Taha |
Concoqtion: indexed types now! |
PEPM |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Zhaozhong Ni, Dachuan Yu, Zhong Shao |
Using XCAP to Certify Realistic Systems Code: Machine Context Management. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
11 | François Garillot, Benjamin Werner |
Simple Types in Type Theory: Deep and Shallow Encodings. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Laurent Théry, Guillaume Hanrot |
Primality Proving with Elliptic Curves. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
11 | David Delahaye, Catherine Dubois, Jean-Frédéric Étienne |
Extracting Purely Functional Contents from Logical Inductive Types. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry |
A Modular Formalisation of Finite Group Theory. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Andrew W. Appel, Sandrine Blazy |
Separation Logic for Small-Step cminor. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Christoph Benzmüller, Dominik Dietrich, Marvin R. G. Schiller, Serge Autexier |
Deep Inference for Automated Proof Tutoring? |
KI |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, Jérôme Vouillon |
A very modal model of a modern, major, general type system. |
POPL |
2007 |
DBLP DOI BibTeX RDF |
impredicative polymorphism, mutable references, recursive types, Kripke models |
11 | Evelyne Contejean |
Modeling Permutations in Coqfor Coccinelle. |
Rewriting, Computation and Proof |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Gilles Barthe, David Pichardie, Tamara Rezk |
A Certified Lightweight Non-interference Java Bytecode Verifier. |
ESOP |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Robert Atkey |
CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. |
TYPES |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa |
Ott: effective tool support for the working semanticist. |
ICFP |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Sylvain Conchon, Jean-Christophe Filliâtre |
A persistent union-find data structure. |
ML |
2007 |
DBLP DOI BibTeX RDF |
formal verification, persistence, union-find |
11 | 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 |
11 | Andrew McCreight, Zhong Shao, Chunxiao Lin, Long Li |
A general framework for certifying garbage collectors and their mutators. |
PLDI |
2007 |
DBLP DOI BibTeX RDF |
assembly code verification, garbage collection, abstract data type, separation logic, proof-carrying code |
11 | Hongxu Cai, Zhong Shao, Alexander Vaynberg |
Certified self-modifying code. |
PLDI |
2007 |
DBLP DOI BibTeX RDF |
assembly code verification, runtime code manipulation, self-modifying code, hoare logic, modular verification |
11 | Xinyu Feng 0001, Zhaozhong Ni, Zhong Shao, Yu Guo |
An open framework for foundational proof-carrying code. |
TLDI |
2007 |
DBLP DOI BibTeX RDF |
foundational proof-carrying code, open framework, interoperability, modularity, program verification |
11 | Nick Benton, Uri Zarfaty |
Formalizing and verifying semantic type soundness of a simple compiler. |
PPDP |
2007 |
DBLP DOI BibTeX RDF |
relational para-metricity, separation logic, proof assistants, compiler verification, type soundness |
11 | J. Santiago Jorge, Víctor M. Gulías, Laura M. Castro |
Verification of Program Properties Using Different Theorem Provers: A Case Study. |
EUROCAST |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Reynald Affeldt, Miki Tanaka, Nicolas Marti |
Formal Proof of Provable Security by Game-Playing in a Proof Assistant. |
ProvSec |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Robert L. Constable, Wojciech Moczydlowski |
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. |
LFCS |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain |
Certification of Automated Termination Proofs. |
FroCoS |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo |
Foundational Typed Assembly Language with Certified Garbage Collection. |
TASE |
2007 |
DBLP DOI BibTeX RDF |
|
11 | David Nowak |
A Framework for Game-Based Security Proofs. |
ICICS |
2007 |
DBLP DOI BibTeX RDF |
security, game, formal verification, proof assistant |
11 | Pierre Corbineau, Cezary Kaliszyk |
Cooperative Repositories for Formal Proofs. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Solange Coupet-Grimal, William Delobel |
An effective proof of the well-foundedness of the multiset path ordering. |
Appl. Algebra Eng. Commun. Comput. |
2006 |
DBLP DOI BibTeX RDF |
Well-foundedness, Multiset path order, Termination, Constructive logic |
11 | Ulrich Berger 0001, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg |
Program Extraction from Normalization Proofs. |
Stud Logica |
2006 |
DBLP DOI BibTeX RDF |
Normalization by evaluation, program extraction from proofs, realizability, typed lambda calculus |
11 | Carlos Simpson |
Explaining Gabriel-Zisman Localization to the Computer. |
J. Autom. Reason. |
2006 |
DBLP DOI BibTeX RDF |
calculus of fractions, computer proof verification, localization, category, proof assistant, functor |
11 | Julien Narboux |
Mechanical Theorem Proving in Tarski's Geometry. |
Automated Deduction in Geometry |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Sandrine-Dominique Gouraud, Arnaud Gotlieb |
Using CHRs to Generate Functional Test Cases for the Java Card Virtual Machine. |
PADL |
2006 |
DBLP DOI BibTeX RDF |
CHR, Java Card Virtual Machine, Software testing |
11 | Nicolas Marti, Reynald Affeldt, Akinori Yonezawa |
Formal Verification of the Heap Manager of an Operating System Using Separation Logic. |
ICFEM |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Sylvie Boldo, César A. Muñoz |
Provably faithful evaluation of polynomials. |
SAC |
2006 |
DBLP DOI BibTeX RDF |
formal verification, floating-point, polynomial evaluation |
11 | Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond |
Assisted verification of elementary functions using Gappa. |
SAC |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Zhaozhong Ni, Zhong Shao |
Certified assembly programming with embedded code pointers. |
POPL |
2006 |
DBLP DOI BibTeX RDF |
embedded code pointers, hoare logic, proof-carrying code, higher-order functions |
11 | Pierre Corbineau |
Deciding Equality in the Constructor Theory. |
TYPES |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli |
Crafting a Proof Assistant. |
TYPES |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Frédéric Besson |
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. |
TYPES |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Frédéric Loulergue |
A calculus of functional BSP programs with projection. |
IPDPS |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Benjamin Grégoire, Laurent Théry |
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Assia Mahboubi |
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Roland Zumkeller |
Formal Global Optimisation with Taylor Models. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz |
Consistency and Completeness of Rewriting in the Calculus of Constructions. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Xinyu Feng 0001, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni |
Modular verification of assembly code with stack-based control abstractions. |
PLDI |
2006 |
DBLP DOI BibTeX RDF |
assembly code verification, control abstractions, stack-based, modularity, proof-carrying code |
11 | Reynald Affeldt, Nicolas Marti |
An Approach to Formal Verification of Arithmetic Functions in Assembly. |
ASIAN |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Devrim Unal, M. Ufuk Çaglayan |
Theorem proving for modeling and conflict checking of authorization policies. |
ISCN |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Benjamin Grégoire, Laurent Théry, Benjamin Werner |
A Computational Approach to Pocklington Certificates in Type Theory. |
FLOPS |
2006 |
DBLP DOI BibTeX RDF |
|
11 | 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 |
|
11 | Sen Xiang, Yiyun Chen, Chunxiao Lin, Long Li |
Modularly Certified Dynamic Storage Allocation in SCAP. |
QSIC |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Nick Benton |
Abstracting Allocation. |
CSL |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Santiago Zanella Béguelin, Gustavo Betarte, Carlos Luna 0001 |
A Formal Specification of the MIDP 2.0 Security Model. |
Formal Aspects in Security and Trust |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Marc Bezem, Thierry Coquand |
Automating Coherent Logic. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Stan Matwin, Amy P. Felty, István T. Hernádvölgyi, Venanzio Capretta |
Privacy in Data Mining Using Formal Methods. |
TLCA |
2005 |
DBLP DOI BibTeX RDF |
|
11 | David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider |
Certified Memory Usage Analysis. |
FM |
2005 |
DBLP DOI BibTeX RDF |
certified memory analysis, Program analysis, theorem proving, constraint solving |
11 | Jean-Pierre Jouannaud |
Higher-Order Rewriting: Framework, Confluence and Termination. |
Processes, Terms and Cycles |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Guillaume Dufay, Amy P. Felty, Stan Matwin |
Privacy-Sensitive Information Flow with JML. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
11 | José Luis Freire, Enrique Freire Brañas, Antonio Blanco |
On Recursive Functions and Well-Founded Relations in the Calculus of Constructions. |
EUROCAST |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Sabrina Tarento |
Machine-Checked Security Proofs of Cryptographic Signature Schemes. |
ESORICS |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Sylvie Boldo, Marc Daumas |
Properties of two's complement floating point notations. |
Int. J. Softw. Tools Technol. Transf. |
2004 |
DBLP DOI BibTeX RDF |
Digital signal processing, Avionics, Formal proof |
11 | Solange Coupet-Grimal, Line Jakubiec |
Certifying circuits in Type Theory. |
Formal Aspects Comput. |
2004 |
DBLP DOI BibTeX RDF |
Co-induction, Formal methods, Type theory, Dependent types, Extraction, Hardware verification |
11 | Olivier Boite |
Proof Reuse with Extended Inductive Types. |
TPHOLs |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Pietro Di Gianantonio, Marino Miculan |
Unifying Recursive and Co-recursive Definitions in Sheaf Categories. |
FoSSaCS |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Solange Coupet-Grimal, William Delobel |
A Uniform and Certified Approach for Two Static Analyses. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Robin Adams 0001 |
Formalized Metatheory with Terms Represented by an Indexed Family of Types. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli |
A Content Based Mathematical Search Engine: Whelp. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Claudio Sacerdoti Coen |
A Semi-reflexive Tactic for (Sub-)Equational Reasoning. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Gilles Barthe, Sabrina Tarento |
A Machine-Checked Formalization of the Random Oracle Model. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Gilles Barthe, Jan Cederquist, Sabrina Tarento |
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|