Bounded-Deducibility Security (Invited Paper) (Englisch)
Freier Zugriff
- Neue Suche nach: Popescu, Andrei
- Weitere Informationen zu Popescu, Andrei:
-
https://orcid.org/0000-0001-8747-0619
- Neue Suche nach: Bauereiss, Thomas
- Neue Suche nach: Lammich, Peter
- Neue Suche nach: Popescu, Andrei
- Weitere Informationen zu Popescu, Andrei:
-
https://orcid.org/0000-0001-8747-0619
- Neue Suche nach: Bauereiss, Thomas
- Neue Suche nach: Lammich, Peter
- Neue Suche nach: Cohen, Liron
- Weitere Informationen zu Cohen, Liron:
-
https://orcid.org/0000-0002-6608-3000
- Neue Suche nach: Kaliszyk, Cezary
- Weitere Informationen zu Kaliszyk, Cezary:
-
https://orcid.org/0000-0002-8273-6059
In:
LIPIcs, Volume 193, ITP 2021
: 12th International Conference on Interactive Theorem Proving (ITP 2021)
;
193
;
3:1-3:20
;
2021
-
ISBN:
-
ISSN:
- Aufsatz (Konferenz) / Elektronische Ressource
-
Titel:Bounded-Deducibility Security (Invited Paper)
-
Beteiligte:Popescu, Andrei ( Autor:in ) / Bauereiss, Thomas ( Autor:in ) / Lammich, Peter ( Autor:in ) / Cohen, Liron ( Herausgeber:in ) / Kaliszyk, Cezary ( Herausgeber:in )
-
Erschienen in:LIPIcs, Volume 193, ITP 2021 : 12th International Conference on Interactive Theorem Proving (ITP 2021) ; 193 ; 3:1-3:20Leibniz International Proceedings in Informatics (LIPIcs) ; 193 ; 3:1-3:20
-
Verlag:
- Neue Suche nach: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
-
Erscheinungsdatum:21.06.2021
-
Format / Umfang:20 pages , 847461 byte
-
Anmerkungen:LIPIcs, Vol. 193, 12th International Conference on Interactive Theorem Proving (ITP 2021), pages 3:1-3:20
-
ISBN:
-
ISSN:
-
DOI:
-
Medientyp:Aufsatz (Konferenz)
-
Format:Elektronische Ressource
-
Sprache:Englisch
-
Schlagwörter:
-
Lizenzbestimmungen:
-
Datenquelle:
Inhaltsverzeichnis Konferenzband
Die Inhaltsverzeichnisse werden automatisch erzeugt und basieren auf den im Index des TIB-Portals verfügbaren Einzelnachweisen der enthaltenen Beiträge. Die Anzeige der Inhaltsverzeichnisse kann daher unvollständig oder lückenhaft sein.
- 1
-
The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper)Myreen, Magnus O. et al. | 2021
- 2
-
Synthesis of Safe Pointer-Manipulating Programs (Invited Talk)Polikarpova, Nadia et al. | 2021
- 3
-
Bounded-Deducibility Security (Invited Paper)Popescu, Andrei / Bauereiss, Thomas / Lammich, Peter et al. | 2021
- 4
-
A Graphical User Interface Framework for Formal VerificationAyers, Edward W. / Jamnik, Mateja / Gowers, W. T. et al. | 2021
- 5
-
A Formalization of Dedekind Domains and Class Groups of Global FieldsBaanen, Anne / Dahmen, Sander R. / Narayanan, Ashvni / Nuccio Mortarino Majno di Capriglio, Filippo A. E. et al. | 2021
- 6
-
A Formally Verified Checker for First-Order ProofsBaek, Seulkee et al. | 2021
- 7
-
Value-Oriented Legal Argumentation in Isabelle/HOLBenzmüller, Christoph / Fuenmayor, David et al. | 2021
- 8
-
Unsolvability of the Quintic Formalized in Dependent Type TheoryBernard, Sophie / Cohen, Cyril / Mahboubi, Assia / Strub, Pierre-Yves et al. | 2021
- 9
-
Itauto: An Extensible Intuitionistic SAT SolverBesson, Frédéric et al. | 2021
- 10
-
Verified Progress Tracking for Timely DataflowBrun, Matthias / Decova, Sára / Lattuada, Andrea / Traytel, Dmitriy et al. | 2021
- 11
-
Syntactic-Semantic Form of Mizar ArticlesByliński, Czesław / Korniłowicz, Artur / Naumowicz, Adam et al. | 2021
- 12
-
Homotopy Type Theory in IsabelleChen, Joshua et al. | 2021
- 13
-
Flexible Coinduction in AgdaCiccone, Luca / Dagnino, Francesco / Zucca, Elena et al. | 2021
- 14
-
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR AlgorithmCordwell, Katherine / Tan, Yong Kiam / Platzer, André et al. | 2021
- 15
-
Formalising a Turing-Complete Choreographic Language in CoqCruz-Filipe, Luís / Montesi, Fabrizio / Peressotti, Marco et al. | 2021
- 16
-
A Natural Formalization of the Mutilated Checkerboard Problem in NaprocheDe Lon, Adrian / Koepke, Peter / Lorenzen, Anton et al. | 2021
- 17
-
A Variant of Wagner’s Theorem Based on Combinatorial HypermapsDoczkal, Christian et al. | 2021
- 18
-
Formalized Haar Measurevan Doorn, Floris et al. | 2021
- 19
-
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-CalculusForster, Yannick / Kunze, Fabian / Smolka, Gert / Wuttke, Maximilian et al. | 2021
- 20
-
Mechanising Complexity Theory: The Cook-Levin Theorem in CoqGäher, Lennard / Kunze, Fabian et al. | 2021
- 21
-
Proving Quantum Programs CorrectHietala, Kesha / Rand, Robert / Hung, Shih-Han / Li, Liyi / Hicks, Michael et al. | 2021
- 22
-
Formalization of Basic Combinatorics on WordsHolub, Štěpán / Starosta, Štěpán et al. | 2021
- 23
-
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in CoqKirst, Dominik / Hermes, Marc et al. | 2021
- 24
-
Complete Bidirectional Typing for the Calculus of Inductive ConstructionsLennon-Bertrand, Meven et al. | 2021
- 25
-
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable NetworksLochbihler, Andreas et al. | 2021
- 26
-
A Formal Proof of Modal Completeness for Provability LogicMaggesi, Marco / Perini Brogi, Cosimo et al. | 2021
- 27
-
Formal Verification of Termination Criteria for First-Order Recursive FunctionsMuñoz, Cesar A. / Ayala-Rincón, Mauricio / Moscato, Mariano M. / Dutle, Aaron M. / Narkawicz, Anthony J. / Almeida, Ariane A. / Avelar, Andréia B. / M. Ferreira Ramos, Thiago et al. | 2021
- 28
-
Verified Double Sided Auctions for Financial MarketsNatarajan, Raja / Sarswat, Suneel / Singh, Abhishek Kr et al. | 2021
- 29
-
Reaching for the Star: Tale of a Monad in CoqNigron, Pierre / Dagand, Pierre-Évariste et al. | 2021
- 30
-
Specifying Message Formats with Contiguity TypesSlind, Konrad et al. | 2021
- 31
-
Proof Pearl : Playing with the Tower of Hanoi FormallyThéry, Laurent et al. | 2021
- 32
-
Verifying an HTTP Key-Value Server with Interaction Trees and VSTZhang, Hengchu / Honoré, Wolf / Koh, Nicolas / Li, Yao / Li, Yishuai / Xia, Li-Yao / Beringer, Lennart / Mansky, William / Pierce, Benjamin / Zdancewic, Steve et al. | 2021