Zobrazeno 1 - 10
of 80
pro vyhledávání: '"Cătălin Hriţcu"'
Autor:
Aseem Rastogi, Cédric Fournet, Karthikeyan Bhargavan, Santiago Zanella-Béguelin, Tahina Ramananandro, Cătălin Hriţcu, Jean Karim Zinzindohoue, Antoine Delignat-Lavaud, Nikhil Swamy, Jonathan Protzenko, Peng Wang
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2017, 1 (ICFP), pp.17:1--17:29. ⟨10.1145/3110261⟩
Proceedings of the ACM on Programming Languages, 2017, 1 (ICFP), pp.17:1--17:29. ⟨10.1145/3110261⟩
22nd International Conference on Functional Programming
Proceedings of the ACM on Programming Languages, ACM, 2017, 1 (ICFP), pp.17:1--17:29. ⟨10.1145/3110261⟩
Proceedings of the ACM on Programming Languages, 2017, 1 (ICFP), pp.17:1--17:29. ⟨10.1145/3110261⟩
22nd International Conference on Functional Programming
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently-typed v
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::08bf5be5baf6171ffa0a43f50c049e47
https://hal.archives-ouvertes.fr/hal-01672706
https://hal.archives-ouvertes.fr/hal-01672706
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2018, 2 (POPL), ⟨10.1145/3158153⟩
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (POPL), ⟨10.1145/3158153⟩
Proceedings of the ACM on Programming Languages, 2018, 2 (POPL), ⟨10.1145/3158153⟩
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (POPL), ⟨10.1145/3158153⟩
We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the current state, provided (1) state evolves according to a given preorde
Publikováno v:
ACM SIGPLAN Notices. 45:105-116
We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calc
Publikováno v:
Interactive Theorem Proving ISBN: 9783319221014
ITP
ITP 2015-6th conference on Interactive Theorem Proving
ITP 2015-6th conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_22⟩
ITP
ITP 2015-6th conference on Interactive Theorem Proving
ITP 2015-6th conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_22⟩
International audience; Integrating property-based testing with a proof assistant creates an interesting opportunity: reusable or tricky testing code can be formally verified using the proof assistant itself. In this work we introduce a novel methodo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d55d2643e1a834aece974af07af08656
https://doi.org/10.1007/978-3-319-22102-1_22
https://doi.org/10.1007/978-3-319-22102-1_22
Autor:
Maxime Dénès, Dimitrios Vytiniotis, John Hughes, Antal Spector-Zabusky, Leonidas Lampropoulos, Arthur Azevedo de Amorim, Benjamin C. Pierce, Cătălin Hriţcu
Publikováno v:
Journal of Functional Programming
Journal of Functional Programming, Cambridge University Press (CUP), 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Journal of Functional Programming, 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Journal of Functional Programming, Cambridge University Press (CUP), 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Journal of Functional Programming, 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Information-flow control mechanisms are difficult both to design and to prove correct. To reduce the time wasted on doomed proof attempts due to broken definitions, we advocate modern random-testing techniques for finding counterexamples during the d
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f9d413c675fd5414f05a7d47c0680d9a
http://arxiv.org/abs/1409.0393
http://arxiv.org/abs/1409.0393
Autor:
Benjamin C. Pierce, Randy Pollack, André DeHon, Andrew Tolmach, Arthur Azevedo de Amorim, Nathan Collins, Delphine Demange, David Pichardie, Cătălin Hriţcu
Publikováno v:
POPL
Journal of Computer Security
Journal of Computer Security, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. ⟨10.1145/2535838.2535839⟩
Journal of Computer Security, IOS Press, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
Journal of Computer Security
Journal of Computer Security, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. ⟨10.1145/2535838.2535839⟩
Journal of Computer Security, IOS Press, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
International audience; SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with effi
Autor:
Cătălin Hriţcu
Publikováno v:
ACM SIGLOG News. 2:23-24
Formal security verification tools are slowly reaching maturity. The Joint EasyCrypt-F*-CryptoVerif School took place between 24 and 28 November 2014 in Paris and taught participants how to use three state-of-the-art security verification tools, as w
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642288906
NASA Formal Methods
NASA Formal Methods
This paper introduces Expi2Java, a new code generator for cryptographic protocols that translates models written in an extensible variant of the Spi calculus into executable code in a substantial fragment of Java, featuring concurrency, synchronizati
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e4a4440ec0b01ca9134fd3eb49afcea3
https://doi.org/10.1007/978-3-642-28891-3_34
https://doi.org/10.1007/978-3-642-28891-3_34