NDLI: From boolean to quantitative synthesis

Please wait, while we are loading the content...

Challenges and potential solutions for complex embedded systems

Heterogeneous actor modeling

Repeatability, reproducibility, and rigor in systems research

Automated distributed implementation of component-based models with priorities

On under-determined dynamical systems

Precise control flow reconstruction using boolean logic

From boolean to quantitative synthesis

Reliability-aware frame packing for the static segment of flexray

Software certification: coding, code, and coders

Demand bound server: generalized resource reservation for hard real-time systems

Cross-layer analysis, testing and verification of automotive control software

Formal verification of hybrid systems

Performance-aware scheduler synthesis for control systems

Symbolic simulation on complicated loops for WCET path analysis

Timing and schedulability analysis for distributed automotive control applications

Resource allocation contracts for open analytic runtime models

RT-Xen: towards real-time hypervisor scheduling in xen

Real-time resource-sharing under clustered scheduling: mutex, reader-writer, and k-exclusion locks

Computing semi-algebraic invariants for polynomial dynamical systems

Automated addition of fault recovery to cyber-physical component-based models

Safety-assured development of the GPCA infusion pump software

Multi-level hierarchical scheduling in ethernet switches

New challenges in certification for aircraft software

Real-time communication analysis for networks with two-stage arbitration

Model-checking behavioral programs

Synchronous control of reconfiguration in fractal component-based systems: a case study

A synergetic approach to accurate analysis of cache-related preemption delay

Time-predictable and composable architectures for dependable embedded systems

A practical ontology framework for static model analysis

Aciom: application characteristics-aware disk and network i/o management on android platform

Task synchronization and allocation for many-core real-time systems

Synthesis of optimal switching logic for hybrid systems

A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous code

Relating average and discounted costs for quantitative analysis of timed systems

Hard-real-time scheduling of data-dependent tasks in embedded streaming applications

Software certification experience in the canadian nuclear industry: lessons for the future

Dynamic scheduling algorithm and its schedulability analysis for certifiable dual-criticality systems

ARMor: fully verified software fault isolation

ExLRU: a unified write buffer cache management for flash memory

Challenges in the regulatory approval of medical cyber-physical systems

From boolean to quantitative synthesis

Content Provider	ACM Digital Library
Author	Černý, Pavol Henzinger, Thomas A.
Abstract	Motivated by improvements in constraint-solving technology and by the increase of routinely available computational power, partial-program synthesis is emerging as an effective approach for increasing programmer productivity. The goal of the approach is to allow the programmer to specify a part of her intent imperatively (that is, give a partial program) and a part of her intent declaratively, by specifying which conditions need to be achieved or maintained. The task of the synthesizer is to construct a program that satisfies the specification. As an example, consider a partial program where threads access shared data without using any synchronization mechanism, and a declarative specification that excludes data races and deadlocks. The task of the synthesizer is then to place locks into the program code in order for the program to meet the specification. In this paper, we argue that quantitative objectives are needed in partial-program synthesis in order to produce higher-quality programs, while enabling simpler specifications. Returning to the example, the synthesizer could construct a naive solution that uses one global lock for shared data. This can be prevented either by constraining the solution space further (which is error-prone and partly defeats the point of synthesis), or by optimizing a quantitative objective that models performance. Other quantitative notions useful in synthesis include fault tolerance, robustness, resource (memory, power) consumption, and information flow.
Starting Page	149
Ending Page	154
Page Count	6
File Format	PDF
ISBN	9781450307147
DOI	10.1145/2038642.2038666
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2011-10-09
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Synthesis Quantitative models Quantitative synthesis
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

From Boolean to quantitative synthesis

From Boolean to quantitative notions of correctness

From quantitative SBML models to boolean networks

From Boolean to quantitative notions of correctness

Predicting genetic interactions from Boolean models of biological networks

Bridging boolean and quantitative synthesis using smoothed proof search

From quantitative SBML to boolean networks

A unified approach to canonical form-based Boolean matching

Efficient solution of systems of Boolean equations

From boolean to quantitative synthesis

Similar Documents

From Boolean to quantitative synthesis

From Boolean to quantitative notions of correctness

From quantitative SBML models to boolean networks

From Boolean to quantitative notions of correctness

Predicting genetic interactions from Boolean models of biological networks

Bridging boolean and quantitative synthesis using smoothed proof search

From quantitative SBML to boolean networks

A unified approach to canonical form-based Boolean matching

Efficient solution of systems of Boolean equations

From boolean to quantitative synthesis