Colloquium
Alexey Solovyev
UNiversity of Pittsburgh
Monday August 12, 2013
3147 MEB
Lecture 2:00 p.m.
Title: Formal Computations and Methods
Alexey Solovyev
UNiversity of Pittsburgh
Monday August 12, 2013
3147 MEB
Lecture 2:00 p.m.
Title: Formal Computations and Methods
Abstract
In my talk, I will present applications of formal methods to mathematical proofs. I will briefly describe the ongoing project on the formal proof of the Kepler conjecture (the Flyspeck project by T. Hales) and my work on a formalization of the computational part of this project. In particular, I will cover formal verification methods and procedures for proving bounds of linear programs and multivariate nonlinear inequalities. Also, I will describe an efficient implementation of interval arithmetic in HOL Light proof assistant.
BIO
Vivek Sarkar conducts research in multiple aspects of parallel software including programming languages, program analysis, compiler optimizations and runtimes for parallel and high performance computer systems. He currently leads the Habanero Multicore Software Research project at Rice University, and serves as Associate Director of the NSF Expeditions project on the Center for Domain-Specific Computing. Prior to joining Rice in July 2007, Vivek was Senior Manager of Programming Technologies at IBM Research. His responsibilities at IBM included leading IBM's research efforts in programming model, tools, and productivity in the PERCS project during 2002- 2007 as part of the DARPA High Productivity Computing System program. His past projects include the X10 programming language, the Jikes Research Virtual Machine for the Java language, the MIT RAW multicore project, the ASTI optimizer used in IBM's XL Fortran product compilers, the PTRAN automatic parallelization system, and profile-directed partitioning and scheduling of Sisal programs. Vivek holds a B.Tech. degree from the Indian Institute of Technology, Kanpur, an M.S. degree from University of Wisconsin-Madison, and a Ph.D. from Stanford University. He became a member of the IBM Academy of Technology in 1995, the E.D. Butcher Chair in Engineering at Rice University in 2007, and was inducted as an ACM Fellow in 2008. Vivek has been serving as a member of the US Department of Energy's Advanced Scientific Computing Advisory Committee (ASCAC) since 2009.
REFERENCES: [1] Habanero Multicore Software Research project. http://habanero.rice.edu
[2] Center for Domain-Specific Computing. http://cdsc.ucla.edu
[3] DARPA Exascale Software Study report, September 2009.
http://users.ece.gatech.edu/~mrichard/ExascaleComputingStudyReports/ECS_reports.htm
[4] DOE report on Synergistic Challenges in Data-Intensive Science and Exascale Computing, March 2013. http://science.energy.gov/~/media/ascr/ascac/pdf/reports/2013/ASCAC_Data_Intensive_Computing_report_final.pdf
Return to 2013 Events Calendar
In my talk, I will present applications of formal methods to mathematical proofs. I will briefly describe the ongoing project on the formal proof of the Kepler conjecture (the Flyspeck project by T. Hales) and my work on a formalization of the computational part of this project. In particular, I will cover formal verification methods and procedures for proving bounds of linear programs and multivariate nonlinear inequalities. Also, I will describe an efficient implementation of interval arithmetic in HOL Light proof assistant.
BIO
Vivek Sarkar conducts research in multiple aspects of parallel software including programming languages, program analysis, compiler optimizations and runtimes for parallel and high performance computer systems. He currently leads the Habanero Multicore Software Research project at Rice University, and serves as Associate Director of the NSF Expeditions project on the Center for Domain-Specific Computing. Prior to joining Rice in July 2007, Vivek was Senior Manager of Programming Technologies at IBM Research. His responsibilities at IBM included leading IBM's research efforts in programming model, tools, and productivity in the PERCS project during 2002- 2007 as part of the DARPA High Productivity Computing System program. His past projects include the X10 programming language, the Jikes Research Virtual Machine for the Java language, the MIT RAW multicore project, the ASTI optimizer used in IBM's XL Fortran product compilers, the PTRAN automatic parallelization system, and profile-directed partitioning and scheduling of Sisal programs. Vivek holds a B.Tech. degree from the Indian Institute of Technology, Kanpur, an M.S. degree from University of Wisconsin-Madison, and a Ph.D. from Stanford University. He became a member of the IBM Academy of Technology in 1995, the E.D. Butcher Chair in Engineering at Rice University in 2007, and was inducted as an ACM Fellow in 2008. Vivek has been serving as a member of the US Department of Energy's Advanced Scientific Computing Advisory Committee (ASCAC) since 2009.
REFERENCES: [1] Habanero Multicore Software Research project. http://habanero.rice.edu
[2] Center for Domain-Specific Computing. http://cdsc.ucla.edu
[3] DARPA Exascale Software Study report, September 2009.
http://users.ece.gatech.edu/~mrichard/ExascaleComputingStudyReports/ECS_reports.htm
[4] DOE report on Synergistic Challenges in Data-Intensive Science and Exascale Computing, March 2013. http://science.energy.gov/~/media/ascr/ascac/pdf/reports/2013/ASCAC_Data_Intensive_Computing_report_final.pdf
Return to 2013 Events Calendar