NDLI: ProofChecker:an accessible environment for automata theory correctness proofs

Content Provider	ACM Digital Library
Author	Stallmann, Matthias F. Balik, Suzanne P. Grace, Michael C. Rodman, Robert D. Bahram, Sina High, Susan D.
Abstract	ProofChecker is a graphical program based on the notion of formal correctness proofs that allows students, both sighted and visually impaired, to draw a deterministic finite automaton (DFA) and determine whether or not it correctly recognizes a given language. Sighted students use the mouse and graphical controls to draw and manipulate the DFA. Keyboard shortcuts, together with the use of a screen reader to voice the accessible descriptions provided by the program, allow visually impaired students to do the same. Because the states of a DFA partition thelanguage over its alphabet into equivalence classes, each state has a language associated with it. Conditions that describe the language of each state are entered by the student in the form of conditional expressions with function calls and/or regular expressions. A brute-force approach is then used to check that each state's condition correctly describes all of the strings in its language and that none of the strings in a state's language meet the condition for another state. Feedback is provided that either confirms that the DFA correctly meets thegiven conditions or alerts the student to a mismatch between the conditions and the DFA. A student's DFA can be saved in an XML file and submitted for grading. An automated checking tool, known as ProofGrader, can be used to compare a student's DFA with the correct DFA for a given language, thus greatly speeding up the grading of student assignments.
Starting Page	48
Ending Page	52
Page Count	5
File Format	PDF
ISSN	00978418
DOI	10.1145/1269900.1268801
Journal	ACM SIGCSE Bulletin (SGCS)
Volume Number	39
Issue Number	3
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1978-02-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Accessibility Finite automata Correctness proof
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

ProofChecker: an accessible environment for automata theory correctness proofs

ABSTRACT ProofChecker: An Accessible Environment for Automata Theory Correctness Proofs

On the Bounds for State-Set Size in the Proofs of Equivalence Between Deterministic, Nondeterministic, and Two-Way Finite Automata

Proof of a program

On the role of proofs in a course on design and analysis of algorithms

Toward compiler implementation correctness proofs

Verifying proofs in constant depth

Correctness proofs of distributed termination algorithms

Rigorous proofs of program correctness without formal logic

ProofChecker:an accessible environment for automata theory correctness proofs

Similar Documents

ProofChecker: an accessible environment for automata theory correctness proofs

ABSTRACT ProofChecker: An Accessible Environment for Automata Theory Correctness Proofs

On the Bounds for State-Set Size in the Proofs of Equivalence Between Deterministic, Nondeterministic, and Two-Way Finite Automata

Proof of a program

On the role of proofs in a course on design and analysis of algorithms

Toward compiler implementation correctness proofs

Verifying proofs in constant depth

Correctness proofs of distributed termination algorithms

Rigorous proofs of program correctness without formal logic

ProofChecker:an accessible environment for automata theory correctness proofs