The 60th GRACE Seminar on Advanced Software Science and Engineering
Time: 13:00-15:00, Jun 13th, 2012
Place:Meeting Room (2009/2010), 20F, National Institute of Informatics（map）
Inquiry: Fuyuki Ishikawa(seminar-steering_AT_nii.ac.jp)
Please register via the following page:
Software quality assurance through formal verification.
Automatic memory safety verification by means of Separation Logic
Monoidics provids advanced code analysis technology focus on memory safety
We’ve achieved the first commercially available automatic verification tool
technology based on Separation Logic, The work on Separation Logic recently was given an award in 2011 by the ACM for ‘Most Influential Paper’ covering the decade.
Like Separation Logic upon which it is based, for Infer, analyzing code is
equivalent to proving a mathematical theorem. If the tool generates a proof for a procedure, it guarantees the procedure is bug-free with respect to memory leaks and errant pointer references.
This contains an overview of bi-abduction (The theoretical notion used by
Infer to automatically synthesize specifications) and compositional anaylsys behind automatic verification.
Dr. Cristiano Calcagno, Monoidics Ltd.
Dr. Peter O’Hearn, Monoidics Ltd.
Dr. Cristiano Calcagno is the Chief Technology Officer and a co-founder of Monoidics. He is a faculty member in the Department of Computing at Imperial College London, and visiting professor at ETH Zurich. Well known in the research world for his work on scalable static analysis algorithms, Calcagno is responsible for leading the execution of technology strategy, research and innovation for Monoidics. He was an Advanced Research Fellow of the Engineering and Physical Sciences Research Council at Imperial College London, and has a PhD in Computer Science from the University of Genova.
Dr. Peter O’Hearn is a Director and a co-founder of Monoidics. He is a Professor of Computer Science at University College London, where he holds a Royal Academy of Engineering/Microsoft Research Chair in Logic and Software Verification. Dr. O’Hearn is a founding inventor of Separation Logic, and his research spans program semantics and mathematical logic through to automated tools for program verification and analysis. His work addresses the 30-year open problem of tractable reasoning about programs that mutate data structures in computer memory. He is the past recipient of the Advanced Research Fellowship from the UK Engineering and Physical Sciences Research Council, the Royal Society Wolfson Research Merit Award, and the Most Influential POPL Paper Award, a 10-year retrospective award given annually for a paper published at the ACM/SIGPLAN Principles of Programming Languages symposium judged to have had the most impact over the past decade. Dr.O’Hearn leads a major UK academic research programme on software verification. He holds a PhD from Queen’s University, Ontario.