Une formalisation fonctionnelle des communications sur la puce

Autor: Schmaltz, J.

Cette thèse présente un modèle formel représentant toute architecture de communication sur la puce. Ce modèle est mathématiquement décrit par une fonction nommée GeNoC. La correction de GeNoC est exprimée par un théorème montrant que tout

Externí odkaz: http://tel.archives-ouvertes.fr/tel-00011526
http://tel.archives-ouvertes.fr/docs/00/05/75/70/PDF/foc_226.pdf

Formal verification of a deadlock detection algorithm

Autor: Verbeek, F., Schmaltz, J., Hardin, D.

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 70, Iss Proc. ACL2 2011, Pp 103-112 (2011)
Hardin, D.; Schmaltz, J. (ed.), Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2011), november 2011, pp. 103-112
Hardin, D.; Schmaltz, J. (ed.), Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2011), november 2011, 103-112. S.l. : s.n.
STARTPAGE=103;ENDPAGE=112;ISSN=2075-2180;TITLE=Hardin, D.; Schmaltz, J. (ed.), Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2011), november 2011

Deadlock detection is a challenging issue in the analysis and design of on-chip networks. We have designed an algorithm to detect deadlocks automatically in on-chip networks with wormhole switching. The algorithm has been specified and proven correct

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6d9a0bde5b02af0e9cd50b594dcb8fd3
https://doaj.org/article/ff6921d65a1a49ae80b39bfe66a87608

Modeling Information Routing with Noninterference

Autor: Koolen, R.P.J., Schmaltz, J.

Publikováno v: International Workshop on MILS: Architecture and Assurance for Secure Systems, Prague, 19 January 2016

To achieve the highest levels of assurance, systems based on the MILS architecture need to be formally analysed. In this, a key challenge is reasoning about the inter-domain flow of information on a finer scale than the domain level. In this paper, w

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5aa69d5547269ed5e4bccfe90c89fb7f

Formal API Specification of the PikeOS Separation Kernel

Autor: Verbeek, F., Havle, O., Schmaltz, J., Tverdyshev, S., Blasum, H., Langenstein, B., Stephan, W., Wolff, B., Nemouchi, Y., Havelund, K., Holzmann, G., Joshi, R.

Publikováno v: Lecture Notes in Computer Science
NASA Formal Methods-7th International Symposium, NFM 2015
NASA Formal Methods-7th International Symposium, NFM 2015, Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi, Apr 2015, Pasadena, CA, USA, France. pp.375--389, ⟨10.1007/978-3-319-17524-9_26⟩
Havelund, K.; Holzmann, G.; Joshi, R. (ed.), NASA Formal Methods : 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, pp. 375-389
Lecture Notes in Computer Science ISBN: 9783319175232
NFM
NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, 375-389
STARTPAGE=375;ENDPAGE=389;TITLE=NASA Formal Methods
Lecture Notes in Computer Science ; 9058, 375-389. Berlin : Springer International Publishing
STARTPAGE=375;ENDPAGE=389;TITLE=Lecture Notes in Computer Science ; 9058
Verbeek, F, Havle, O, Schmaltz, J, Tverdyshev, S, Blasum, H, Langenstein, B, Werner, S, Wolff, B & Nemouchi, Y 2015, Formal API Specification of the PikeOS Separation Kernel . in K Havelund, G Holzmann & R Joshi (eds), NASA Formal Methods : 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings . Springer International Publishing AG, Cham, Lecture Notes in Computer Science (LNCS) series, no. 9058, Programming and Software Engineering LNPSE, vol. 9058, pp. 375-389, 7th NASA Formal Methods Symposium, Pasadena, United States, 27/04/15 . https://doi.org/10.1007/978-3-319-17524-9_26

PikeOS is an industrial operating system for safety and security critical applications in, for example, avionics and automotive contexts. A consortium of several European partners from industry and academia works on the certification of PikeOS up to

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6fa5d6a773db1c731aea92a8a77bf08e
https://hal.inria.fr/hal-01275405

Logical Formalisation and Analysis of the Mifare Classic Card in PVS

Autor: Jacobs, B., Schreur, R. Wichers, Eekelen, M. van, Geuvers, H., Schmaltz, J., Wiedijk, F.

Publikováno v: Eekelen, M. van; Geuvers, H.; Schmaltz, J. (ed.), Interactive Theorem Proving, pp. 3-17
Interactive Theorem Proving ISBN: 9783642228629
ITP
Lecture Notes in Computer Science ; 6898, 3-17. Berlin / Heidelberg : Springer
STARTPAGE=3;ENDPAGE=17;TITLE=Lecture Notes in Computer Science ; 6898

The way that Mifare Classic smart cards work has been uncovered recently [6,8] and several vulnerabilities and exploits have emerged. This paper gives a precise logical formalisation of the essentials of the Mifare Classic card, in the language of a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::83ecf2e2daf2e397f9c4c218bd5b035e
https://hdl.handle.net/2066/92012