Student Seminar and Bowling Night
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
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 https://github.com/SpencerPark/MellowD 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.