Student Seminar and Bowling Night

ITB 201

We will be having another LICS graduate seminar August 17th, 2017 in ITB 201 from 2:30 - 3:30. Refreshments will be provided! Our speakers will be Spencer Park and Nicholas Moore.

Following the seminar, you are welcome to join us for Bowling at University Lanes from 4:30 - 6:00! Admission and shoe rentals are free, though no outside food or drink is allowed in the bowling alley. University Lanes is located at University Plaza, a short bus ride from Campus.


Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving

Nicholas Moore: PhD Student


FPGAs are increasingly prevelant in PLC applications, but existing formal verification of PLC programs is not fully applicable to new architectural styles. We aim to produce a library of formally verified PLC function blocks for FPGA platforms. To this end, we propose a new method for embedding Bluespec SystemVerilog descriptions in PVS's higher-order proof logic. In contrast to previous embeddings, our approach accepts a greater subset of BSV and provides a far greater degree of automation. Our custom software tool transforms the action-oriented semantics of BSV to a state-centric Kripke structure, enabling automated theorem proving. We demonstrate our verification techique by applying it to one of the function blocks of the IEC 61131-3 standard for PLCs.

Music Compiler and High Level Language for Music Compilation

Spencer Park

GitHub source

I have been working on a music compiler that started as a school project but became a fun project to work on. If you are interested the source is on github but the documentation is missing at the moment. It's essentially a language that compiles into an audio file similar to programs that take sheet music and preform it but the syntax is much closer to a scripting language.