Logical Foundations: Simple Imperative Programs
Presenter: Traian Serbanuta. This week we continue exploring Coq based on the Logical Foundations volume of Software Foundations, chapter "IMP: Simple Imperative Programs"
10 events found.
Events
-
-
Facultatea de Matematica si Informatica, sala 202
-
The finitary content of sunny nonexpansive retractions
Facultatea de Matematica si Informatica, sala 202Andrei Sipoș (TU Darmstadt & IMAR). The goal of proof mining is to extract quantitative information out of proofs in mainstream mathematics which are not necessarily fully constructive. Often, such proofs make use of strong mathematical principles, but a preliminary analysis may show that they are not actually needed, so the proof may be carried …
-
Logical Foundations: Simple Imperative Programs – variables and commands
Facultatea de Matematica si Informatica, sala 202Presenter: Traian Serbanuta. This week we continue exploring Coq based on the Logical Foundations volume of Software Foundations, chapter "IMP: Simple Imperative Programs"
-
-
Making Obsolete Malware Viable with Packing
Facultatea de Matematica si Informatica, sala 202Speaker: Mihai Stancu Abstract: The security trend today is to stop security threats even before they arrive on the target machine or system. With that in mind we will explore, what packers are and what they do to transform original malicious code in into something that is much harder to confidently mark as a threat. …
-
The frontier between decidability and undecidability for logics for strategic reasoning in the presence of imperfect information
Facultatea de Matematica si Informatica, sala GoogleSpeaker: Catalin Dima (Université Paris-Est Créteil.) Abstract: The last 15-20 years have seen a number of logical formalisms that focus on strategic reasoning. These logics aim at giving specification languages for various multi-agent game structures, in which agents have adversarial or cooperative objectives which may be qualitative or quantitative and may have various types of …
-
-
Verification of strategic properties for the Prêt-À-Voter protocol using Tamarin (joint work with Wojtek Jamroga and Damian Kurpiewski)
Facultatea de Matematica si Informatica, sala GoogleSpeaker: Catalin Dima (Université Paris-Est Créteil) Abstract: We report on the verification of anonymity and coercion-freeness properties of the Prêt-À-Voter electronic voting protocol using the Tamarin tool for symbolic verification of security properties. Our approach is to generate many models corresponding with each choice of attacker actions (i.e. attacker strategies) and check, on each model, a "trace equivalence" lemma modeling the fact that the …
-
Criptosistemul lui McEliece, dupa 40 de ani de criptanaliza
Facultatea de Matematica si Informatica, sala 220 Strada Academiei 14, Bucuresti, Bucuresti, RomaniaSpeaker: Vlad Dragoi (Univ. Aurel Vlaicu Arad) Abstract: Aceasta prezentare are ca scop descrierea principalelor solutii de criptare asimetrica cu ajutorul codurilor corectoare de erori. Vom incerca sa discutam cat mai multe aspecte legate de aceste protocoale, cum ar fi: natura codurilor folosite in acest context, complexitatea algoritmilor de criptare si decriptare, securitatea protocolului (distinguisher, message …
-
Security aspects for blockchain
Facultatea de Matematica si Informatica, sala 202Speaker: Andreea Elena Panait (University of Bucharest). Abstract: The presentation will include introductive notions about blockchain, the main types of attacks on the blockchain network and possible countermeasures, attack examples that occurred during the years, blockchain implementation examples and possible domains where blockchain can be used.
-
Security via user behavior
Facultatea de Matematica si Informatica, sala 202Speaker: Cezara Benegui (University of Bucharest). Abstract: The presentation will be based on earlier research done on user behaviour understanding and detection, learning it using machine learning and artificial intelligence and further information about how user behaviour can be used to improve the security of software applications. Also, the presentation will include information about biometrics …
-
The hybridization of many-sorted polyadic modal logic
Speaker: Natalia Moangă (University of Bucharest). Abstract: Hybrid logics are obtained by enriching modal logics with nominals and state variables, that directly refer the individual points in a Kripke model. In the present work we develop a hybrid version on top of our many-sorted polyadic logic, previously defined. Our system has nominals and state variables …