[cs-talks] Upcoming Seminars: Ph.D Proposal (Tues) + iBench (Thurs)

cs, Group cs at bu.edu
Tue Mar 31 10:51:42 EDT 2015

Ph.D Proposal
Terrier: A real-time, embedded operating system using advanced types for safety
Matthew Danish, BU
Tuesday, March 31, 2015 at 3:20pm in MCS 148

Abstract:  Operating systems software is fundamental to modern computer systems: all other applications are dependent upon the correct and timely provision of basic system services. At the same time, advances in programming languages and type theory have lead to the creation of functional programming languages with type systems that are designed to combine theorem proving with practical systems programming. The Terrier operating system project focuses on doing low-level systems programming in the context of a multi-core, real-time, embedded system, while taking advantage of a dependently typed programming language named ATS to improve reliability. Terrier is a new point in the design space for an operating system, one that leans heavily on an associated programming language, ATS, to provide safety that has traditionally been in the scope of hardware protection and kernel privilege. Terrier tries to have far fewer abstractions between program and hardware. The purpose of Terrier is to put programs as much in contact with the real hardware, real memory, and real timing constraints as possible, while still retaining the ability to multiplex programs and provide for a reasonable level of safety through static analysis. Committee: Hongwei Xi Richard West Chris Hawblitzel Assaf Kfoury Ibrahim Matta.

An Overview of Knowledge Compilation for Solving #SAT and its Applications to Cybersecurity
Richard W. Skowyra, Technical Staff, Cyber Systems and Technology Group, MIT Lincoln Laboratory
Thursday, April 2, 2015 at 12:30pm in MCS B21

Abstract: Boolean model counting, referred to as #SAT, is the problem of determining for a given formula the number of satisfying truth assignments to its variables. Many real-world problem domains are inherently beyond the ability of modern SAT solvers despite being semantically amenable to modeling as a Boolean formula, as the quality of a solution may depend not only on satisfying the formula but also on the total number of satisfying solutions that exist under some constraint. In this talk I will provide a motivating example from the cybersecurity domain and discuss a knowledge compilation approach to solving #SAT developed by Adnan Darwiche. His Decomposable Deterministic Negation Normal Form (D-DNNF) encodes a Boolean formula in a directed graph which admits polynomial time model counting and output-linear time model enumeration. I will conclude with some lessons learned while implementing a tool for translating a domain-specific modeling and query language to and from D-DNNF.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs-mailman.bu.edu/pipermail/cs-talks/attachments/20150331/c6d2649f/attachment.html>

More information about the cs-talks mailing list