[11-21]Adventures in Code Generation

文章来源:  |  发布时间:2016-11-16  |  【打印】 【关闭


    Title: Adventures in Code Generation 

    Speaker: Dr. Natarajan Shankar,  Principal scientist of Stanford Research Institute (SRI) International 

    Time: 15:30pm, Monday, Nov. 21, 2016 

    Venue: Room 334, Building 5, State Key Lab. of Computer Science, Institute of Software 


  PVS is an interactive proof assistant based on higher-order logic. We describe the PVS2C code generator which produces C code from an executable, functional subset of the PVS specification language. Typechecking in PVS ensures that a well-typed program will not trigger any runtime error such as a buffer overflow or an uncaught exception. It can fail only by exhausting stack or heap bounds. PVS2C handles a significant subset of PVS including datatypes, closures, and functional updates (for sparse or infinite arrays). The main novelty in PVS2C is that it uses reference counting as a mechanism for managing memory and implementing applicative updates with minimal copying. Code generation is factored through an intermediate language based on A-normal form.

  This yields efficient, safe, and self-contained code that does not require a runtime or a garbage collector. The talk presents the background theory, the ongoing formalization of this theory in PVS itself, a demo of PVS2C on some illustrative examples, and plans for future work.

    Short bio of the speaker: 

  Dr. Natarajan Shankar is a Principal Scientist at SRI International. He has worked there since 1989 and was made an SRI Fellow in 2009. He has a Ph.D. in Computer Science from the University of Texas at Austin. His research interests include automated reasoning, formal methods, computational logic, programming language theory, and artificial intelligence.

  He, along with his SRI colleagues, has developed of a number of logic-based tools, including the PVS interactive proof assistant, the SAL model checker, the Yices SMT solver, the PCE probabilistic inference engine, and the Radler architecture definition language for cyber-physical systems.