arXiv subjects

Manuel Oriol

Publications and source records attributed to Manuel Oriol.

17 recordsLinked to original sources

arXiv2026

Modeling Quantum Computing with $π$-calculus

Quantum computing is a difficult concept to grasp for computer scientists because it is full of mathematical formulas that have no intuitive meaning related to the problem that the code solves. While these formulae define the way the system behaves, the operational semantics is very far from regular programming languages that reason with variables, assignments, and passing by value the results of computation. This article takes a step back to define a theoretical framework where quantum programs are not treated as sequential programs, but rather as concurrent programs where variables advertise their states through their own channels and code that uses them is reading that state (and possibly collapsing it). The PiQuant framework is a simple extension of the $π$-calculus that contains additional syntax and semantics for the handling of quantum variables.

cs.PL↗

arXiv2026

ReqFusion: A Multi-Provider Framework for Automated PEGS Analysis Across Software Domains

Requirements engineering is a vital, yet labor-intensive, stage in the software development process. This article introduces ReqFusion: an AI-enhanced system that automates the extraction, classification, and analysis of software requirements utilizing multiple Large Language Model (LLM) providers. The architecture of ReqFusion integrates OpenAI GPT, Anthropic Claude, and Groq models to extract functional and non-functional requirements from various documentation formats (PDF, DOCX, and PPTX) in academic, industrial, and tender proposal contexts. The system uses a domain-independent extraction method and generates requirements following the Project, Environment, Goal, and System (PEGS) approach introduced by Bertrand Meyer. The main idea is that, because the PEGS format is detailed, LLMs have more information and cues about the requirements, producing better results than a simple generic request. An ablation study confirms this hypothesis: PEGS-guided prompting achieves an F1 score of 0.88, compared to 0.71 for generic prompting under the same multi-provider configuration. The evaluation used 18 real-world documents to generate 226 requirements through automated classification, with 54.9% functional and 45.1% nonfunctional across academic, business, and technical domains. An extended evaluation on five projects with 1,050 requirements demonstrated significant improvements in extraction accuracy and a 78% reduction in analysis time compared to manual methods. The multi-provider architecture enhances reliability through model consensus and fallback mechanisms, while the PEGS-based approach ensures comprehensive coverage of all requirement categories.

cs.SE↗

arXiv2026

Combining Tests and Proofs for Better Software Verification

Test or prove? These two approaches to software verification have long been presented as opposites. One is dynamic, the other static: a test executes the program, a proof only analyzes the program text. A different perspective is emerging, in which testing and proving are complementary rather than competing techniques for producing software of verified quality. Work performed over the past few years and reviewed here develops this complementarity by taking advantage of Design by Contract, as available in Eiffel, and exploiting a feature of modern program-proving tools based on ``Satisfiability Modulo Theories'' (SMT): counterexample generation. A counterexample is an input combination that makes the program fail. If we are trying to prove a program correct, we hope not to find any. One can, however, apply counterexample generation to incorrect programs, as a tool for automatic test generation. We can also introduce faults into a correct program and turn the counterexamples into an automatically generated regression test suite with full coverage. Additionally, we can use these mechanisms to help produce program fixes for incorrect programs, with a guarantee that the fixes are correct. All three applications, leveraging on the mechanisms of Eiffel and Design by Contract, hold significant promise to address some of the challenges of program testing, software maintenance and Automatic Program Repair.

cs.SE↗

arXiv2025

Architecture for a Trustworthy Quantum Chatbot

Large language model (LLM)-based tools such as ChatGPT seem useful for classical programming assignments. The more specialized the field, the more likely they lack reliability because of the lack of data to train them. In the case of quantum computing, the quality of answers of generic chatbots is low. C4Q is a chatbot focused on quantum programs that addresses this challenge through a software architecture that integrates specialized LLMs to classify requests and specialized question answering modules with a deterministic logical engine to provide trustworthy quantum computing support. This article describes the latest version (2.0) of C4Q, which delivers several enhancements: ready-to-run Qiskit code for gate definitions and circuit operations, expanded features to solve software engineering tasks such as the travelling salesperson problem and the knapsack problem, and a feedback mechanism for iterative improvement. Extensive testing of the backend confirms the system's reliability, while empirical evaluations show that C4Q 2.0's classification LLM reaches near-perfect accuracy. The evaluation of the result consists in a comparative study with three existing chatbots highlighting C4Q 2.0's maintainability and correctness, reflecting on how software architecture decisions, such as separating deterministic logic from probabilistic text generation impact the quality of the results.

cs.CL↗

arXiv2024

Is ChatGPT 3 safe for students?

ChatGPT3 is a chat engine that fulfils the promises of an AI-based chat engine: users can ask a question (prompt) and it answers in a reasonable manner. The coding-related skills of ChatGPT are especially impressive: informal testing shows that it is difficult to find simple questions that ChatGPT3 does not know how to answer properly. Some students are certainly already using it to answer programming assignments. This article studies whether it is safe for students to use ChatGPT3 to answer coding assignments (safe means that they will not be caught for plagiarism if they use it). The main result is that it is generally not safe for students to use ChatGPT3. We evaluated the safety of code generated with ChatGPT3, by performing a search with a Codequiry, a plagiarism detection tool, and searching plagiarized code in Google (only considering the first page of results). In 38% of the cases, Codequiry finds a piece of code that is partially copied by the answer of ChatGPT3. In 96% of the cases, the Google search finds a piece of code very similar to the generated code. Overall, it is not safe for students to use ChatGPT3 in 96% of the cases.

cs.SE↗

arXiv2024

Benefits and Risks of Using ChatGPT4 as a Teaching Assistant for Computer Science Students

Upon release, ChatGPT3.5 shocked the software engineering community by its ability to generate answers to specialized questions about coding. Immediately, many educators wondered if it was possible to use the chatbot as a support tool that helps students answer their programming questions. This article evaluates this possibility at three levels: fundamental Computer Science knowledge (basic algorithms and data structures), core competency (design patterns), and advanced knowledge (quantum computing). In each case, we ask normalized questions several times to ChatGPT3.5, then look at the correctness of answers, and finally check if this creates issues. The main result is that the performances of ChatGPT3.5 degrades drastically as the specialization of the domain increases: for basic algorithms it returns answers that are almost always correct, for design patterns the generated code contains many code smells and is generally of low quality, but it is still sometimes able to fix it (if asked), and for quantum computing it is often blatantly wrong.

cs.CY↗

arXiv2024

Quantum types: going beyond qubits and quantum gates

Quantum computing is a growing field with significant potential applications. Learning how to code quantum programs means understanding how qubits work and learning to use quantum gates. This is analogous to creating classical algorithms using logic gates and bits. Even after learning all concepts, it is difficult to create new algorithms, which hinders the acceptance of quantum programming by most developers. This article outlines the need for higher-level abstractions and proposes some of them in a developer-friendly programming language called Rhyme. The new quantum types are extensions of classical types, including bits, integers, floats, characters, arrays, and strings. We show how to use such types with code snippets.

quant-ph↗

arXiv2024

Execution-free Program Repair

Automatic program repair usually relies heavily on test cases for both bug identification and fix validation. The issue is that writing test cases is tedious, running them takes much time, and validating a fix through tests does not guarantee its correctness. The novel idea in the Proof2Fix methodology and tool presented here is to rely instead on a program prover, without the need to run tests or to run the program at all. Results show that Proof2Fix finds and fixes significant historical bugs.

cs.SE↗

arXiv2024

C4Q: A Chatbot for Quantum

Quantum computing is a growing field that promises many real-world applications such as quantum cryptography or quantum finance. The number of people able to use quantum computing is however still very small. This limitation comes from the difficulty to understand the concepts and to know how to start coding. Therefore, there is a need for tools that can assist non-expert in overcoming this complexity. One possibility would be to use existing conversational agents. Unfortunately ChatGPT and other Large-Language Models produce inaccurate results. This article presents C4Q, a chatbot that answers accurately basic questions and guides users when trying to code quantum programs. Contrary to other approaches C4Q uses a pre-trained large language model only to discover and classify user requests. It then generates an accurate answer using an own engine. Thanks to this architectural design, C4Q's answers are always correct, and thus C4Q can become a support tool that makes quantum computing more available to non-experts.

cs.CL↗

arXiv2023

Seeding Contradiction: a fast method for generating full-coverage test suites

The regression test suite, a key resource for managing program evolution, needs to achieve 100% coverage, or very close, to be useful. Devising a test suite manually is unacceptably tedious, but existing automated methods are often inefficient. The method described in this article, ``Seeding Contradiction'', inserts incorrect instructions into every basic block of the program, enabling an SMT-based Hoare-style prover to generate a counterexample for every branch of the program and, from the collection of all such counterexamples, a test suite. The method is static, works fast, and achieves excellent coverage.

cs.SE↗

arXiv2022

Improving Counterexample Quality from Failed Program Verification

In software verification, a successful automated program proof is the ultimate triumph. The road to such success is, however, paved with many failed proof attempts. The message produced by the prover when a proof fails is often obscure, making it very hard to know how to proceed further. The work reported here attempts to help in such cases by providing immediately understandable counterexamples. To this end, it introduces an approach called Counterexample Extraction and Minimization (CEAM). When a proof fails, CEAM turns the counterexample model generated by the prover into a a clearly understandable version; it can in addition simplify the counterexamples further by minimizing the integer values they contain. We have implemented the CEAM approach as an extension to the AutoProof verifier and demonstrate its application to a collection of examples.

cs.SE↗

arXiv2015

Stochastic Contracts for Runtime Checking of Component-based Real-time Systems

This paper introduces a new technique for dynamic verification of component-based real-time systems based on statistical inference. Verifying such systems requires checking two types of properties: functional and real-time. For functional properties, a standard approach for ensuring correctness is Design by Contract: annotating programs with executable pre- and postconditions. We extend contracts for specifying real-time properties. In the industry, components are often bought from vendors and meant to be used off-the-shelf which makes it very difficult to determine their execution times and express related properties. We present a solution to this problem by using statistical inference for estimating the properties. The contract framework allows application developers to express contracts like "the execution time of component $X$ lies within $γ$ standard deviations from the mean execution time". Experiments based on industrial case studies show that this framework can be smoothly integrated into existing control applications, thereby increasing their reliability while having an acceptable execution time overhead (less than 10%).

cs.SE↗

arXiv2014

Execution Time Analysis for Industrial Control Applications

Estimating the execution time of software components is often mandatory when evaluating the non-functional properties of software-intensive systems. This particularly holds for real-time embedded systems, e.g., in the context of industrial automation. In practice it is however very hard to obtain reliable execution time estimates which are accurate, but not overly pessimistic with respect to the typical behavior of the software. This article proposes two new concepts to ease the use of execution time analysis for industrial control applications: (1) a method based on recurring occurrences of code sequences for automatically creating a timing model of a given processor and (2) an interactive way to integrate execution time analysis into the development environment, thus making timing analysis results easily accessible for software developers. The proposed methods are validated by an industrial case study, which shows that a significant amount of code reuse is present in a set of representative industrial control applications.

cs.SE↗

arXiv2013

C to O-O Translation: Beyond the Easy Stuff

Can we reuse some of the huge code-base developed in C to take advantage of modern programming language features such as type safety, object-orientation, and contracts? This paper presents a source-to-source translation of C code into Eiffel, a modern object-oriented programming language, and the supporting tool C2Eif. The translation is completely automatic and supports the entire C language (ANSI, as well as many GNU C Compiler extensions, through CIL) as used in practice, including its usage of native system libraries and inlined assembly code. Our experiments show that C2Eif can handle C applications and libraries of significant size (such as vim and libgsl), as well as challenging benchmarks such as the GCC torture tests. The produced Eiffel code is functionally equivalent to the original C code, and takes advantage of some of Eiffel's object-oriented features to produce safe and easy-to-debug translations.

cs.PL↗

arXiv2012

The Search for the Laws of Automatic Random Testing

Can one estimate the number of remaining faults in a software system? A credible estimation technique would be immensely useful to project managers as well as customers. It would also be of theoretical interest, as a general law of software engineering. We investigate possible answers in the context of automated random testing, a method that is increasingly accepted as an effective way to discover faults. Our experimental results, derived from best-fit analysis of a variety of mathematical functions, based on a large number of automated tests of library code equipped with automated oracles in the form of contracts, suggest a poly-logarithmic law. Although further confirmation remains necessary on different code bases and testing techniques, we argue that understanding the laws of testing may bring significant benefits for estimating the number of detectable faults and comparing different projects and practices.

cs.SE↗

arXiv2012

Class Schema Evolution for Persistent Object-Oriented Software: Model, Empirical Study, and Automated Support

With the wide support for object serialization in object-oriented programming languages, persistent objects have become common place and most large object-oriented software systems rely on extensive amounts of persistent data. Such systems also evolve over time. Retrieving previously persisted objects from classes whose schema has changed is however difficult, and may lead to invalidating the consistency of the application. The ESCHER framework addresses these issues through an IDE-integrated approach that handles class schema evolution by managing versions of the code and generating transformation functions automatically. The infrastructure also enforces class invariants to prevent the introduction of potentially corrupt objects. This article describes a model for class attribute changes, a measure for class evolution robustness, four empirical studies, and the design and implementation of the ESCHER system.

cs.SE↗

arXiv2009

The Business of Selling Electronic Documents

The music industry has huge troubles adapting to the new technologies. As many pointed out, when copying music is essentially free and socially accepted it becomes increasingly tempting for users to infringe copyrights and copy music from one person to another. The answer of the music industry is to outlaw a majority of citizens. This article describes how the music industry should reinvent itself and adapt to a world where the network is ubiquitous and exchanging information is essentially free. It relies on adapting prices to the demand and lower costs of electronic documents in a dramatic way.

cs.GL↗