Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13,2013, ProceedingsGeorges Gonthier, Michael Norrish Springer, 11 de des. 2013 - 309 pàgines This book constitutes the refereed proceedings of the Third International Conference on Certified Programs and Proofs, CPP 2013, colocated with APLAS 2013 held in Melbourne, Australia, in December 2013. The 18 revised regular papers presented together with 1 invited lecture were carefully reviewed and selected from 39 submissions. The papers are organized in topical sections on code verification, elegant proofs, proof libraries, certified transformations and security. |
Altres edicions - Mostra-ho tot
Certified Programs and Proofs: Third International Conference, Cpp 2013 ... Georges Gonthier,Michael Norrish Previsualització no disponible - 2013 |
Certified Programs and Proofs: Third International Conference, CPP 2013 ... Georges Gonthier,Michael Norrish Previsualització no disponible - 2013 |
Frases i termes més freqüents
abstract type algorithm automata bad sequence bignum bisimilarity bisimulation bool closure conversion co-inductive CompCert compiler computation construction constructor context contrasimulation corresponding datatype defined definition DFAs discr encode environment equivalence example execution finite formalization function Heidelberg Hoare logic Hoare triple homotopy Horn clauses htrms implementation induction initial instantiated integer intOp Isabelle/HOL lemma LLVM LNCS logic loop loop space lterm machine code matrix memory model minimal Myhill-Nerode theorem NetCore nfa1 nfa2 noninterference notion operational semantics operations package packets param parametricity parse tree pointer predicate properties prove quotient RC-Model reachable recursive refinement regular expressions regular languages relation representation result role rules SAFECode semantics simulation siso sound specification Springer string tainted target termination theorem transfer transition type system type theory typechecker up-to variables verified