Logical Foundations: Total and Partial Maps
Speaker: Miriam Costan. This week we continue exploring Coq based on the Logical Foundations volume of Software Foundations, chapter "Total and Partial Maps"
10 events found.
Events
-
-
Facultatea de Matematica si Informatica, sala 202
-
How to find bugs in your (x86) code; RIVER tool – current state and future
Facultatea de Matematica si Informatica, sala 202Speaker: Ciprian Păduraru Abstract: Even with access to the source code of a program, it is not easy to reverse engineer a program to find inputs for specific programs. This presentation starts with a practical walkthrough over classic methods for automating software testing, such as fuzz testing, symbolic and concolic execution. Then, a tool named …
-
Logical Foundations: Simple Imperative Programs
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"
-
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.