Real Quantifier Elimination for the Verification and Synthesis of Systems and Algorithms
Mădălina Eraşcu
Institute e-Austria, Timişoara, Romania
DEIB - Seminar Room
May 4th, 2015
11.00 am
Contacts:
Matteo Giovanni Rossi
Research Line:
Advanced software architectures and methodologies
Institute e-Austria, Timişoara, Romania
DEIB - Seminar Room
May 4th, 2015
11.00 am
Contacts:
Matteo Giovanni Rossi
Research Line:
Advanced software architectures and methodologies
Sommario
Real quantifier elimination is a fundamental problem in mathematical logic and computational real algebraic geometry. Furthermore, it naturally arises in many challenging problems in diverse application areas. Due to its importance, there has been extensive research on developing mathematical theories, efficient algorithms, software systems, and applications.
In this talk we present applications of real quantifier elimination in three contexts.
First, we investigate methods for synthesizing optimal algorithms. As a case study, we consider the square root problem: given the real number x and the error bound Ɛ, find a real interval such that it contains √x and its width is less than Ɛ. We use iterative refining as algorithm schema: the algorithm starts with an initial interval and repeatedly updates it by applying a refinement map, say ƒ; on it until it becomes narrow enough. Then the synthesis amounts to finding a refinement map ƒ that ensures that the algorithm is correct (loop invariant), terminating (contraction), and optimal. All these could be formulated as quantifier elimination over the real numbers. Hence, in principle, they could be performed automatically. However, the computational requirement is huge, making the automatic synthesis practically impossible with the current general quantifier elimination software. Therefore, we performed some hand derivations and were able to synthesize semi-automatically optimal algorithms under natural assumptions. (Joint work with Hoon Hong)
Second, we exemplify how hierarchical reasoning and real quantifier elimination can be applied to verification problems for parametric reactive and hybrid systems. More precisely, we analyze the possibility of automatically generating safety or invariance conditions in the form of constraints on parameters (constants or functions), then show that we can also synthesize so-called criticality functions, typically used for proving stability and/or safety of hybrid systems. (Joint work with Viorica Sofronie-Stokkermans)
Last, we present some ideas on how real quantifier elimination (existential fragment), could be useful in the negotiation of security service level objectives of Cloud services.
This work is performed in the framework of SPECS project (http://specs-project.eu/).
In this talk we present applications of real quantifier elimination in three contexts.
First, we investigate methods for synthesizing optimal algorithms. As a case study, we consider the square root problem: given the real number x and the error bound Ɛ, find a real interval such that it contains √x and its width is less than Ɛ. We use iterative refining as algorithm schema: the algorithm starts with an initial interval and repeatedly updates it by applying a refinement map, say ƒ; on it until it becomes narrow enough. Then the synthesis amounts to finding a refinement map ƒ that ensures that the algorithm is correct (loop invariant), terminating (contraction), and optimal. All these could be formulated as quantifier elimination over the real numbers. Hence, in principle, they could be performed automatically. However, the computational requirement is huge, making the automatic synthesis practically impossible with the current general quantifier elimination software. Therefore, we performed some hand derivations and were able to synthesize semi-automatically optimal algorithms under natural assumptions. (Joint work with Hoon Hong)
Second, we exemplify how hierarchical reasoning and real quantifier elimination can be applied to verification problems for parametric reactive and hybrid systems. More precisely, we analyze the possibility of automatically generating safety or invariance conditions in the form of constraints on parameters (constants or functions), then show that we can also synthesize so-called criticality functions, typically used for proving stability and/or safety of hybrid systems. (Joint work with Viorica Sofronie-Stokkermans)
Last, we present some ideas on how real quantifier elimination (existential fragment), could be useful in the negotiation of security service level objectives of Cloud services.
This work is performed in the framework of SPECS project (http://specs-project.eu/).
Biografia
Mădălina ERAŞCU has been a postdoctoral researcher at Institute e-Austria, since February 2014. Prior to this, she had been a postdoctoral researcher at the Department of Computer Science, West University of Timisoara, Romania and in the Theorema group at Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria.
Her research interests are Distributed Computing (Cloud Computing), Automated Theorem Proving (First-Order Theorem Proving) and Symbolic Computation (Polynomial Algebra). More precisely, she is interested in developing algorithmic methods for building and maintaining reliable algorithms. To achieve this goal, she combines theoretical research motivated by practical applications in formal methods, automated theorem proving and computer algebra. Recently she started investigating Cloud Computing and Big Data fields and tries to apply her earlier expertise in these exciting research areas.
She holds a PhD in Technical Sciences from Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria. Her PhD thesis was advised by Professor Tudor Jebelean and Professor Hoon Hong and deals with the (semi-)automatic analysis and synthesis of programs using computational logic and polynomial algebra algorithms. She also holds a M.Sc. from Johannes Kepler University (2008) and a B.Sc. from West University of Timisoara (2006), both in computer science. Her master's and bachelor's theses were partly realized in the framework of the software companies Mindbreeze Software GmbH and, respectively, SC memIQ SRL.
In 2010, she was awarded the competitive DOC-fFORTE-fellowship of the Austrian Academy of Sciences (June 2011 - November 2012). In the framework of Marshall Plan Foundation scholarship, she spent five months (January - June 2011) at North Carolina State University, Raleigh, USA, working under the supervision of Professor Hoon Hong.
Her research interests are Distributed Computing (Cloud Computing), Automated Theorem Proving (First-Order Theorem Proving) and Symbolic Computation (Polynomial Algebra). More precisely, she is interested in developing algorithmic methods for building and maintaining reliable algorithms. To achieve this goal, she combines theoretical research motivated by practical applications in formal methods, automated theorem proving and computer algebra. Recently she started investigating Cloud Computing and Big Data fields and tries to apply her earlier expertise in these exciting research areas.
She holds a PhD in Technical Sciences from Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria. Her PhD thesis was advised by Professor Tudor Jebelean and Professor Hoon Hong and deals with the (semi-)automatic analysis and synthesis of programs using computational logic and polynomial algebra algorithms. She also holds a M.Sc. from Johannes Kepler University (2008) and a B.Sc. from West University of Timisoara (2006), both in computer science. Her master's and bachelor's theses were partly realized in the framework of the software companies Mindbreeze Software GmbH and, respectively, SC memIQ SRL.
In 2010, she was awarded the competitive DOC-fFORTE-fellowship of the Austrian Academy of Sciences (June 2011 - November 2012). In the framework of Marshall Plan Foundation scholarship, she spent five months (January - June 2011) at North Carolina State University, Raleigh, USA, working under the supervision of Professor Hoon Hong.
