Poster

file

Visible to the public The Molecular Programming Project- Molecular Programming Architectures, Abstractions, Algorithms, and Applications

Submitted by Eric Klavins on Wed, 07/10/2019 - 2:02pm. Contributors:

Our Expeditions in Computing aimed to establish the foundations for molecular programming as a new discipline within computer science. A molecular program is a collection of molecules that may perform a computation, fabricate an object, or control a system of molecular sensors and actuators.

file

Visible to the public The Molecular Programming Project: Molecular Programming Architectures, Abstractions, Algorithms, and Applications

Submitted by William Shih on Wed, 07/10/2019 - 1:46pm. Contributors:

Our Expeditions in Computing aimed to establish the foundations for molecular programming as a new discipline within computer science. A molecular program is a collection of molecules that may perform a computation, fabricate an object, or control a system of molecular sensors and actuators.

file

Visible to the public Computational Sustainability: Computational Methods for a Sustainable Environment, Economy, and Society

Submitted by Carla Gomes on Wed, 07/10/2019 - 1:02pm. Contributors:

Poverty, saving species, repowering the world with renewable energy, lifting people up to live better lives - there are no easy answers to guiding our planet on a path toward sustainability. Complex problems require sophisticated solutions. They involve intricacy beyond human capabilities, the kind of big-data processing and analysis that only advanced large-scale computing can provide.

file

Visible to the public Reasoning with Assurance Arguments under Uncertainty – Composing Formal and Non-Formal

Submitted by akarns on Thu, 05/09/2019 - 1:50pm. Contributors:

A significant challenge in automating certification of software intensive complex computing systems is information heterogeneity that runs the gamut from non-formal artifacts such as safety analyses, operational guidance, unit tests, and simulation runs to, more recently, formal artifacts. An emerging approach to certification of such software systems is the use of assurance cases to provide goal-based arguments supported by evidence.

file

Visible to the public Affix: Binary Model Generation for Static Analysis

Submitted by mwhicks1 on Wed, 05/08/2019 - 3:20pm. Contributor:

Static analysis and dynamic analysis are the yin and yang of program analysis. Static analysis has the benefit that it can reason about many, or all, runs of a program at once. However, to do that it must abstract aspects of the programs semantics. For large or complicated programs, the resulting imprecision can lead to an intolerable number of false-positive alarms. Dynamic analysis reasons about particular program executions precisely, using a (perhaps automatically generated) test suite.

file

Visible to the public ACE Assurance, Composed, and Explained

Submitted by pranavsrinivas on Wed, 05/08/2019 - 2:42pm. Contributors:

The state-of-the-art in systems assurance is based on testing, simulation and certification, and it is currently incorporating formal verification for some of the system's components. Formal verification has a limited use at present because it calls for a clean slate design and development, which are not always possible or practical, and because it is computationally challenging for large systems. Therefore, formal verification is commonly constrained to single software or hardware components that can be adequately modeled.

file

Visible to the public Integrated Data Space Randomization and Control Reconfiguration for Securing Cyber-Physical Systems

Submitted by Bradley Potteiger on Wed, 05/08/2019 - 2:42pm. Contributors:

Cyber-Physical Systems (CPS) have been increasingly subject to cyber-attacks including code Non-control data attacks have become widely popular for circumventing authentication mechanisms in websites, servers, and personal computers. Moreover, in the context of Cyber-Physical Systems (CPS) attacks can be executed against not only authentication but also safety. With the tightly coupled nature between the cyber components and physical dynamics, any unauthorized change to safety-critical variables may cause damage or even catastrophic consequences.

file

Visible to the public Practical Application of SPARK to OpenUxAS: Initial Results

Submitted by Anonymous on Wed, 05/08/2019 - 2:42pm. Contributors:

Formal methods provide powerful tools for the analysis of complex software, enabling engineers to establish assurance of high quality in their software. The SPARK language and tools build upon the foundation of Ada and allow engineers to program not only their software, but also their specifications and their proofs. SPARK thus provides engineers a practical, industrial strength formal method.