Introductory programming courses often rely on numerous exercises to help students practice and reinforce their skills. Commonly used automated tests fall short by merely identifying the issues without offering guidan...
详细信息
ISBN:
(纸本)9798400712166
Introductory programming courses often rely on numerous exercises to help students practice and reinforce their skills. Commonly used automated tests fall short by merely identifying the issues without offering guidance on how to resolve them and manual reviews are too resource-intensive to use in large classes. To address these challenges, we present ASSIST-a tool designed to provide automated, detailed feedback on how to resolve issues in programming exercise submissions with both syntactic and logical errors. ASSIST combines fault-tolerant parsing with fixes based on the context of error nodes to resolve syntactic errors and give feedback. ASSIST feeds this valid program to the Sketch program synthesis tool to determine the needed changes from a set of potential changes induced by rewrite rules, and generates feedback on logic errors based on the needed changes. This dual approach allows ASSIST to offer actionable feedback on both syntax and logic issues in student submissions. We evaluated ASSIST on submissions from an online platform for secondary education. Our findings reveal that, for submissions with syntax errors, ASSIST delivers feedback on all syntax errors in 71% of cases and extends its feedback to cover logical errors in 34% of these submissions. When evaluating all incorrect submissions, ASSIST is able to give feedback on logical errors in 64% of cases. These results indicate that ASSIST can significantly enhance the feedback process in large-scale programming courses, offering a feasible and efficient alternative to current methods.
This paper presents some ideas concerning program manipulation and program transformation from the early days of their development. Particular emphasis will be given to program transformation techniques in the area of...
详细信息
The proceedings contain 32 papers. The special focus in this conference is on programming. The topics include: Formulas as Processes, Deadlock-Freedom as Choreographies;Sufficient Conditions for Robustness of RDMA Pro...
ISBN:
(纸本)9783031911170
The proceedings contain 32 papers. The special focus in this conference is on programming. The topics include: Formulas as Processes, Deadlock-Freedom as Choreographies;Sufficient Conditions for Robustness of RDMA Programs;Constructive characterisations of the MUST-preorder for asynchrony;abstraction of memory block manipulations by symbolic loop folding;cognacy Queries over Dependence Graphs for Transparent Visualisations;an abstract, certified account of operational game semantics;artifact Report: an Abstract, Certified Account of Operational Game Semantics;neural Network Verification is a programming Language Challenge;stratified Type Theory;coverage Semantics for Dependent Pattern Matching;variable Elimination as Rewriting in a Linear Lambda Calculus;a Program logic for Concurrent Randomized Programs in the Oblivious Adversary Model;iso-Recursive Multiparty Sessions and their Automated Verification;verifying Algorithmic Versions of the Lovász Local Lemma;Elucidating Type Conversions in SQL Engines.
The proceedings contain 32 papers. The special focus in this conference is on programming. The topics include: Formulas as Processes, Deadlock-Freedom as Choreographies;Sufficient Conditions for Robustness of RDMA Pro...
ISBN:
(纸本)9783031911200
The proceedings contain 32 papers. The special focus in this conference is on programming. The topics include: Formulas as Processes, Deadlock-Freedom as Choreographies;Sufficient Conditions for Robustness of RDMA Programs;Constructive characterisations of the MUST-preorder for asynchrony;abstraction of memory block manipulations by symbolic loop folding;cognacy Queries over Dependence Graphs for Transparent Visualisations;an abstract, certified account of operational game semantics;artifact Report: an Abstract, Certified Account of Operational Game Semantics;neural Network Verification is a programming Language Challenge;stratified Type Theory;coverage Semantics for Dependent Pattern Matching;variable Elimination as Rewriting in a Linear Lambda Calculus;a Program logic for Concurrent Randomized Programs in the Oblivious Adversary Model;iso-Recursive Multiparty Sessions and their Automated Verification;verifying Algorithmic Versions of the Lovász Local Lemma;Elucidating Type Conversions in SQL Engines.
A day in the life of a developer often involves more time working with schemas, configurations, and data description systems than writing code and logic in a classical programming language. As more systems move into d...
详细信息
ISBN:
(纸本)9798400712159
A day in the life of a developer often involves more time working with schemas, configurations, and data description systems than writing code and logic in a classical programming language. As more systems move into distributed worlds, e.g. cloud and microservices, and developers make increasing use of libraries and frameworks, the need to interact with a range of data formats and configuration mechanisms is only increasing. This is a treacherous world, where a misspelled property name or missing field can render an entire service inoperable, a mistake that a number in an API represents seconds instead of milli-seconds can lead to a message being set for delivery in several months instead of in an hour, misconfigured schema can lead to public exposure of sensitive data, and corrupt or erroneous results from a misunderstood data format could result in massive financial and/or reputational damage. To address these challenges this paper casts the problems of data and configuration descriptions, not as a problem of data representation, but as a type system problem, that can be addressed with well understood and highly effective programming language techniques! The novel challenge is that data representation and configuration are universal concerns in a system and, particularly in modern cloud or micro-service systems, these systems may involve many programming languages. In the past this has led to specification systems that use a least-common-denominator set of data types, often little more than strings and numbers, and then rely on conventions or (out-of-date) documentation to ensure that the data is interpreted correctly. This paper shows that, with careful design, it is possible to create a rich universal system that can be used to express data and configuration specifications in a way that is human readable/writable and that can be produced/consumed, much like JSON, by a wide range of programming languages and systems.
One approach to explaining the hierarchical levels of understanding within a machine learning model is the symbolic method of inductive logicprogramming (ILP), which is data efficient and capable of learning first-or...
详细信息
The proceedings contain 13 papers. The topics discussed include: a calculus of delayed reductions;multicompatibility for multiparty-session composition;termination in concurrency, revisited;typed equivalence of labele...
ISBN:
(纸本)9798400708121
The proceedings contain 13 papers. The topics discussed include: a calculus of delayed reductions;multicompatibility for multiparty-session composition;termination in concurrency, revisited;typed equivalence of labeled effect handlers and labeled delimited control operators;type-directed program transformation for constant-time enforcement;comprehending queries over finite maps;intuitionistic metric temporal logic;strongly-typed multi-view stack-based computations;and polymorphic typestate for session types;additive cellular automata graded-monadically.
Adiabatic quantum-flux parametron (AQFP) is a superconducting technology with extremely low power consumption compared to traditional CMOS structure. Since AQFP logic gates are all clocked by AC current, extra buffer ...
详细信息
This system demonstration presents Nemo, a new logicprogramming engine with a focus on reliability and performance. Nemo is built for data-centric analytic computations, modelled in a fully declarative Datalog dialec...
详细信息
This system demonstration presents Nemo, a new logicprogramming engine with a focus on reliability and performance. Nemo is built for data-centric analytic computations, modelled in a fully declarative Datalog dialect. Its scalability for these tasks matches or exceeds that of leading Datalog systems. We demonstrate uses in reasoning with knowledge graphs and ontologies with 10(5)-10(8) input facts, all on a laptop. Nemo is written in Rust and available as a free and open source tool.
The proceedings contain 20 papers. The topics discussed include: UTC time, formally verified;VCFloat2: floating-point error analysis in coq;the last yard: foundational end-to-end verification of high-speed cryptograph...
ISBN:
(纸本)9798400704888
The proceedings contain 20 papers. The topics discussed include: UTC time, formally verified;VCFloat2: floating-point error analysis in coq;the last yard: foundational end-to-end verification of high-speed cryptography;rooting for efficiency: mechanized reasoning about array-based trees in separation logic;compositional verification of concurrent C programs with search structure templates;unification for subformula linking under quantifiers;PfComp: a verified compiler for packet filtering leveraging binary decision diagrams;memory simulations, security and optimization in a verified compiler;lean formalization of extended regular expression matching with lookarounds;certification of confluence- and commutation-proofs via parallel critical pairs;a temporal differential dynamic logic formal embedding;and strictly monotone Brouwer trees for well-founded recursion over multiple arguments.
暂无评论