NDLI logo
  • Content
  • Similar Resources
  • Metadata
  • Cite This
  • Log-in
  • Fullscreen
Log-in
Do not have an account? Register Now
Forgot your password? Account recovery
  1. Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH Companion 2016)
  2. The science of deep specification (keynote)
Loading...

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

The science of deep specification (keynote)
Dedicated support for analyses and optimizations in language workbenches
Introducing lightweight reactive values to Java
Design pattern builder: a concept for refinable reusable design pattern libraries
A human view of programming languages (keynote)
Integrating concerns with development environments
Specifying CSS layout with reference attribute grammars
End-user software engineering of cognitive robot applications using procedural parameters and complex event processing
Language support for verifiable SDNs
Reconsidering reliability in distributed actor systems
A compiler for linear algebra operations
VeriTaS: verification of type system specifications: mechanizing domain knowledge about progress and preservation proofs
Supporting resource bounded multitenancy in Akka
An approach to compile configurable systems with #ifdefs based on impact analysis
Scaling testing of refactoring engines
A web application is a domain-specific language
Flexible initialization of immutable objects
Multitier reactive abstractions
A sampling-based approach to accelerating queries in log management systems
Finding concurrency bugs using graph-based anomaly detection in big code
Spray: programming with a persistent distributed heap
sk_p: a neural program corrector for MOOCs
Reducing procedure call bloat in ARM binaries
Towards practical release-level dynamic software updating on stock Java: evaluating an efficient and safely programmable Java dynamic updating system
libDSU: towards hot-swapping dynamically linked libraries on stock Linux
PixelDust: supporting dynamic area of interest tagging in programming studies with eye tracking
Removing stagnation from modern code review
Improving live debugging of concurrent threads
xWIDL: modular and deep JavaScript API misuses checking based on extended WebIDL
Towards object-aware development tools
Deducing classes: integrating the domain models of object-oriented applications
Energy profiling with Alpaca
Scrambler: dynamic layout adaptation

Similar Documents

...
QuickChick: A Coq Framework For Verified Property-Based Testing (2014)

Thesis

...
QuickChick: Property-Based Testing for Coq (2014)

...
QuickChick : Property-Based Testing for Coq

Article

...
Verified peephole optimizations for CompCert

Article

...
Formalizing the LLVM Intermediate Representation for Verified Program Transformations (2012)

Article

...
Formalizing the LLVM Intermediate Representation for Verified Program Transformations (2012)

Proceeding

...
Verified peephole optimizations for CompCert

Article

...
A Coq Framework For Verified Property-Based Testing Internship Report (2014)

...
A Coq Framework For Verified Property-Based Testing ( Extended Abstract )

Article

The science of deep specification (keynote)

Content Provider ACM Digital Library
Author Pierce, Benjamin C.
Abstract Abstraction and modularity underlie all successful hardware and software systems: We build complex artifacts by decomposing them into parts that can be understood separately. Modular decomposition depends crucially on the artful choice of interfaces between pieces. As these interfaces become more expressive, we think of them as specifications of components or layers. Rich specifications based on formal logic are little used in industry today, but a practical platform for working with them could signicantly reduce the costs of system implementation and evolution by identifying vulnerabilities, helping programmers understand the behavior of new components, facilitating rigorous change-impact analysis, and supporting maintainable machine-checked verication that components are correct and fit together correctly. Recently, research in the area has begun to focus on a particularly rich class of specifications, which might be called deep specifications. Deep specifications are rich (describing complex component behaviors in detail); two-sided (connected to both implementations and clients); formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs); and live (connected directly to the source code of implementations via machine-checkable proofs or property-based random testing). These requirements impose strong functional correctness conditions on individual components and permit them to be connected together with rigorous composition theorems. This talk presents the key features of deep specifications, surveys recent achievements and ongoing efforts in the research community (in particular, work at Penn, Princeton, Yale, and MIT on formalizing a rich interconnected collection of deep specifications for critical system software components), and argues that the time is ripe for an intensive effort in this area, involving both academia and industry and integrating research, education, and community building. The ultimate goal is to provide rigorously checked proofs about much larger artifacts than are feasible today, based on decomposition of proof effort across components with deep specifications. .
Starting Page 1
Ending Page 1
Page Count 1
File Format PDF
ISBN 9781450344371
DOI 10.1145/2984043.2998388
Language English
Publisher Association for Computing Machinery (ACM)
Publisher Date 2016-10-20
Publisher Place New York
Access Restriction Subscribed
Subject Keyword Kami Coq Vellvm Verified software toolchain Verified systems software Compcert Certikos Property-based testing Quickchick
Content Type Text
Resource Type Article
  • About
  • Disclaimer
  • Feedback
  • Sponsor
  • Contact
  • Chat with Us
About National Digital Library of India (NDLI)
NDLI logo

National Digital Library of India (NDLI) is a virtual repository of learning resources which is not just a repository with search/browse facilities but provides a host of services for the learner community. It is sponsored and mentored by Ministry of Education, Government of India, through its National Mission on Education through Information and Communication Technology (NMEICT). Filtered and federated searching is employed to facilitate focused searching so that learners can find the right resource with least effort and in minimum time. NDLI provides user group-specific services such as Examination Preparatory for School and College students and job aspirants. Services for Researchers and general learners are also provided. NDLI is designed to hold content of any language and provides interface support for 10 most widely used Indian languages. It is built to provide support for all academic levels including researchers and life-long learners, all disciplines, all popular forms of access devices and differently-abled learners. It is designed to enable people to learn and prepare from best practices from all over the world and to facilitate researchers to perform inter-linked exploration from multiple sources. It is developed, operated and maintained from Indian Institute of Technology Kharagpur.

Learn more about this project from here.

Disclaimer

NDLI is a conglomeration of freely available or institutionally contributed or donated or publisher managed contents. Almost all these contents are hosted and accessed from respective sources. The responsibility for authenticity, relevance, completeness, accuracy, reliability and suitability of these contents rests with the respective organization and NDLI has no responsibility or liability for these. Every effort is made to keep the NDLI portal up and running smoothly unless there are some unavoidable technical issues.

Feedback

Sponsor

Ministry of Education, through its National Mission on Education through Information and Communication Technology (NMEICT), has sponsored and funded the National Digital Library of India (NDLI) project.

Contact National Digital Library of India
Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302
See location in the Map
03222 282435
Mail: support@ndl.gov.in
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
I will try my best to help you...
Cite this Content
Loading...