Zobrazeno 1 - 10
of 21
pro vyhledávání: '"Cătălin Hriţcu"'
Autor:
Catalin Hritcu, Jan Schwinghammer
Publikováno v:
Logical Methods in Computer Science, Vol Volume 5, Issue 4 (2009)
Step-indexed semantic interpretations of types were proposed as an alternative to purely syntactic proofs of type safety using subject reduction. The types are interpreted as sets of values indexed by the number of computation steps for which these v
Externí odkaz:
https://doaj.org/article/c1499712fdea4cc1b05f60d3b71c053f
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