On Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments
Graph Chatbot
Chattez avec Graph Search
Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.
AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.
Context: The number of students enrolled in universities at standard and on-line programming courses is rapidly increasing. This calls for automated evaluation of students assignments. Objective: We aim to develop methods and tools for objective and reljab ...
Generic code increases programmer productivity as it increases code reuse. For example, the LinkedList abstraction can be used in many contexts, from storing a list of numbers to storing representations of files on the disk. Unfortunately this comes at the ...
Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way—they should succeed for a well-defin ...
Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succ ...
Testing of critical PLC (Programmable Logic Controller) programs remains a challenging task for control system engineers as it can rarely be automated. This paper proposes a model-based approach which uses the BIP (Behavior, Interactions and Priorities) fr ...
MadX (Methodical Accelerator Design) is the de-facto standard software for modeling accelerator lattices at CERN. This feature-rich software package is implemented and still maintained in the programming languages C and FORTRAN. Nevertheless the controls e ...
Safety-critical software systems can only support a limited number of failures. Extensive testing is good at catching errors, however that will never certify their absence. Formal verification is an alternative to testing that can (automatically) provide a ...
Virtualization-obfuscation protects a program from manual or automated analysis by compiling it into bytecode for a randomized virtual architecture and attaching a corresponding interpreter. Static analysis appears to be helpless on such programs, where on ...
Systematic State Exploration or Model Checking techniques have been used for years to check the model of softwares against user-specified properties. Nevertheless, they never achieved a wide-spread usage because of the difficulties and problems in translat ...
Current state-of-the-art static analysis tools for binary software operate on ad-hoc intermediate representations (IR) of the machine code. Therefore, even though IRs facilitate program analysis by abstracting away the source language, it is hard to reuse ...