Les outils d’aide à la preuve basés sur la théorie des types permettent à l’utilisateur d’adopter soit un style fonctionnel, soit un style relationnel (c’est-à-dire en utilisant des types inductifs). Chacun des deux styles a des avantages et des inconvénients. Le style relationnel peut être préféré parce qu’il permet à l’utilisateur de décrire seulement ce qui est vrai, de s’abstraire temporairement de la question de la terminaison, et de s’en tenir à une description utilisant des règles. Cependant, une spécification relationnelle n’est pas exécutable.Nous proposons un cadre général pour transformer une spécification inductive en une spécification fonctionnelle, en extrayant à partir de la première une fonction et en produisant éventuellement la preuve de correction de la fonction extraite par rapport à sa spécification inductive. De plus, à partir de modes définis par l’utilisateur, qui permettent de considérer les arguments de la relation comme des entrées ou des sorties (de fonction), nous pouvons extraire plusieurs comportements calculatoires à partir d’un seul type inductif.Nous fournissons également deux implantations de notre approche, l’une dans l’outil d’aide à la preuve Coq et l’autre dans l’environnement Focalize. Les deux sont actuellement distribuées avec leurs outils respectifs. / Proof assistants based on type theory allow the user to adopt either a functional style, or a relational style (e.g., by using inductive types). Both styles have advantages and drawbacks. Relational style may be preferred because it allows the user to describe only what is true, discard momentarily the termination question, and stick to a rule-based description. However, a relational specification is usually not executable.We propose a general framework to turn an inductive specification into a functional one, by extracting a function from the former and eventually produce the proof of soundness of the extracted function w.r.t. its inductive specification. In addition, using user-defined modes which label inputs and outputs, we are able to extract several computational contents from a single inductive type.We also provide two implementations of our approach, one in the Coq proof assistant and the other in the Focalize environnement. Both are currently distributed with the respective tools.

The main focus of this dissertation thesis is on methods and tools which can increase the speed of software development process for embedded processors used in mechatronics applications. The first part of this work introduces software and hardware tools suitable for a rapid development and prototyping of new applications used today. This work focuses on two main topics from the mentioned application field. The first topic is a development of tools for an automatic code generation from the Simulink environment for an embedded processor. The second topic is a development of tools enabling execution time prediction based on a Simulink model. Next chapter of this work describes various aspects and properties of the Cerebot blockset, which is a toolset for a fully automatic code generation from a Simulink environment for an embedded processor. Following chapter describes various methods that are suitable for predicting the execution time on an embedded processor based on a Simulink model. Main contribution of this work presents the created support for a fully automatic code generation from a Simulink software for the MX7 cK hardware, which enables a code generation supporting also a complex peripheral (a graphic display unit). The next important contribution of this work presents the developed method for an automatic prediction of the software execution time based on a Simulink model.

Usage of natural language processing tools to generate code is increasing together with the advances in artificial intelligence. These tools could improve the efficiency of software development, if the generated code can be shown to be trustworthy enough to solve a given problem. This thesis examines what problems can be solved using automatically generated code such that the results can be trusted. A set of six problems were chosen to be used for testing two automatic code generators and the accuracy of their generated code. The problems were chosen to span a range from introductory programming assignments to complex problems with no known efficient algorithm. The problems also varied in how direct their descriptions were, with some describing exactly what should be done, while others described a real-world scenario with a desired result. The problems were used as prompts to the automatic code generators to generate code in three different programming languages. A testing framework was built that could execute the generated code, feed problem instances to the processes, and then verify the solutions that were outputted from them. The data from these tests were then used to calculate the accuracy of the generated code, based on how many of the problem instances were correctly solved. The experimental results show that most solutions to the problems either got all outputs correct, or had few or no correct outputs. Problems with direct explanations, or simple and well known algorithms, such as sorting, resulted in code with high accuracy. For problems that were wrapped in a scenario, the accuracy was the lowest. Hence, we believe that identifying the underlying problem before resorting to code generators should possibly increase the accuracy of the code. / Användningen av verktyg som bygger på språkteknologi för att generera kod har ökat i takt med framstegen inom artificiell intelligens. Dessa verktyg kan användas för att öka effektiviten inom mjukvaruutveckling, om den genererade koden kan visas tillförlitlig nog för att lösa ett givet problem. Denna avhandling utforskar vilka problem som kan lösas med automatiskt genererad kod på en nivå sådan att resultaten kan dömas tillförlitliga. En mängd på sex olika problem valdes för att testa två olika kodgenererande verktygs noggrannhet. De utvalda problemen valdes för att täcka ett stort span av programmeringsproblem. Från grundläggande programmeringsproblem till komplexa problem utan kända effektiva algoritmer. Problemen hade även olika nivåer av tydlighet i deras beskrivning. Vissa problem var tydligt formulerade med ett efterfrågat tillvägagångssätt, andra var mindre tydliga med sitt respektive förväntade resultat inbakat i problembeskrivningen. De utvalda kodgenererade verktygen uppmanades lösa problem enligt sex problembeskrivningar på tre olika programmeringsspråk. Ett ramverk byggdes som skapade probleminstanser, exekverade den genererade koden och verifierade den utmatade lösningen. Resultaten användes för att beräkna den genererade kodens noggrannhet, baserat på hur många av de givna instanserna som lösts korrekt. Resultaten från testerna visar att de flesta av de genererade lösningarna fick antingen alla eller inga instanser korrekt lösta. Problem med tydliga beskrivningar och enkla välkända algoritmer så som sortering, resulterade i kod med hög noggrannhet. För de mindre tydliga problemen, som resulterade i lägst noggrannhet, bör identifiering av det underliggande problemet öka kodens noggrannhet.

ChatGPT has made large language models more accessible and made it possible to code using natural language prompts. This study conducted an experiment comparing prompt engineering techniques called task specification and investigated their impacton code generation in terms of correctness and variety. The hypotheses of this study focused on whether the baseline method had a statistically significant difference in code correctness compared to the other methods. Code is evaluated using a software requirement specification that measures functional and syntactical correctness. Additionally, code variance is measured to identify patterns in code generation. The results show that there is a statistically significant difference in some code correctness criteria between the baseline and the other task specification methods, and the code variance measurements indicate a variety in the generated solutions. Future work could include using another large language model; different programming tasks andprogramming languages; and other prompt engineering techniques.

<p>Static program analyzers are vital tools to produce useful insights about programs without executing these programs. These insights can be used to improve the quality of programs, e.g., detecting defects in programs, or optimizing programs to use fewer resources. However, building static program analyzers that are simultaneously sound, performant, and flexible is notoriously challenging.</p> <p>This dissertation aims to address this challenge by exploring the potential of applying correct-by-construction metaprogramming techniques to build static program analyzers. Metaprogramming techniques manipulate and transform programs as data objects.  In this thesis, we consider static program analyzers as the objects to be manipulated or transformed. We show that metaprogramming techniques can improve our understanding, the construction, flexibility, and performance of program analyzers.</p> <p>We first study the inter-derivation of abstract interpreters. Using off-the-shelf program transformation techniques such as refunctionalization, we demonstrate that big-step abstract interpreters can be mechanically derived from their small-step counterparts, thus building a functional correspondence between two different styles of abstract interpretation.</p> <p>To build high-performance program analyzers, we exploit the first Futamura projection to build compilers for abstract interpretation and symbolic execution. The first Futamura projection states that specializing an interpreter with respect to an input program is a process equivalent to compilation, thus providing a practical way to repurpose interpreters for compilation and code generation. We systematically apply this idea to build program-analysis compilers by writing analyzers as staged interpreters using higher-level abstractions. The staged interpreter can be used for generating sound and performant analysis code given a specific input program. Moreover, the approach enables using abstractions without regret: by using higher-level program abstractions, the analyzer can be written in a way that is close to its high-level specification (e.g. big-step operational semantics), and by compilation, the analyzer is performant since it does not need to pay the runtime overhead of using these abstraction mechanisms.</p> <p>We also develop novel type systems that track sharing and separation in higher-order imperative languages. Such type systems are useful both for general-purpose programming languages and for optimization of domain-specific metaprograms such as those program-analysis compilers.</p> <p><br></p>

The electric vehicle industry is experiencing a boom infunding and public interest, and the formula student movementis following suit; an electric race car is currently being developedby the KTH Formula Student organisation (KTHFS) which is thecause of this work.Consumers desire increased speed and range, and are unwillingto compromise one quality for the other. This necessitates the useof lithium ion cells, which may explode and exhume toxic gasesif over-strained with respect to current, charge or temperature.A robust, reliable and provably safe battery management systemshould therefore be developed. There are numerous methods tofurther increase the mileage to get an edge on competitors, suchas cell balancing and live estimation of the State of Charge(SOC). It is also vital that old and/or deteriorated cells should beidentified and disposed off in due time, and State of health (SOH)estimation provides a means to do this. In this paper a completebattery management system software solution is developed andpresented, utilising methods like simulation and code generationto create a program that runs on a real time operating system(RTOS). Some real world test were conducted and some resultsare simulated. The finished BMS performed well in tests, meets allgoals and meets all timing constraints. The project can thereforebe considered as successful. / Intresset för elbilsindustrin har på sistone‌ vuxit något markant, och formula student-rörelsen har anpassat sig efter dessa trender; en elektriskt bil tillverkas just nu av KTH Formula Student organisationen (KTHFS) vilket ger upphov till detta arbete. Marknaden vill ha snabbare bilar som dessutom har förbättrad räckvidd, men vägrar offra den ena egenskapen för det andra. Lösningen är att använda litiumjonceller. Dessa har dock en säkerhetsrelaterad nackdel; om cellerna utsätts för alldeles för höga eller låga temperaturer, strömmar eller laddningsnivåer kan de explodera och utsöndra giftig gas i luften. Därför är det lämpligt att skapa ett batterimonitoreringssystem vars funktion och säkerhet kvalitativt kan utvärderas och bevisas. Det finns flera metoder för att få förbättrad prestanda ur sin ackumulator (batteriensemble); cellnivåbalansering och laddningsnivåestimering (SOC) implementeras i detta projekt. Föråldrade/utslitna celler bör identifieras och avskrivas i god tid. Celldeklineringsestimering (SOH) är ett sätt att lösa detta problem. I denna rapport presenteras en fullständig implementation av mjukvaran för ett batterimonitoreringssystem, där metoder som kodgenerering och simulering utnyttjas för att skapa ett program som kan köras på ett realtidsoperativsystem (RTOS). Vissa test gjordes i verkligheten och vissa resultat simulerades. Det färdiga batterimonitoreringssystemet presterade väl i test, alla mål samt mötte alla tidskrav. Projektet kan därför anses som lyckat. / Kandidatexjobb i elektroteknik 2022, KTH, Stockholm

Continuous Deep Analytics (CDA) is a new form of analytics with performance requirements exceeding what the current generation of distributed systems can offer. This thesis is part of a five year project in collaboration between RISE SICS and KTH to develop a next generation distributed system capable of CDA. The two issues which the system aims to solve are computation sharing and hardware acceleration. The former refers to how BigData and machine learning libraries such as TensorFlow, Pandas and Numpy must collaborate in the most efficient way possible. Hardware acceleration relates to how the back-end of current generation general purpose data processing systems such as Spark and Flink are bottlenecked by the Java Virtual Machine (JVM). As the JVM abstracts over the underlying hardware, its applications become portable but also forfeit the opportunity to fully exploit the available hardware resources. This thesis aims to explore the area of Domain Specific Languages (DSLs) and code generation as a solution to hardware acceleration. The idea is to translate incoming queries to the system into low-level code, tailor suited to each worker machine’s specific hardware. To this end, two Scala DSLs for generating Rust code have been developed for the translation step. Rust is a new, low-level programming language with a unique take on memory management which makes it as safe as Java and fast as C. Scala is a language which is well suited towards development of DSLs due to its flexible syntax and semantics. The first DSL is implemented as a string interpolator. The interpolator splices strings of Rust code together, at compile time or runtime, and passes the result to an external process for static checking. The second DSL instead provides an API for constructing an abstract syntax tree, which after construction can be traversed and printed into Rust source code. The API combines three concepts: heterogeneous lists, fluent interfaces, and algebraic data types. These allow the userto express advanced Rust syntax such as polymorphic structs, functions, and traits, without sacrificing type safety. / Kontinuerlig Djup Analys (CDA) är en ny form av analys med prestandakrav som överstiger vad den nuvarande generationen av distributerade system kan erbjuda. Den här avhandlingen är del av ett project mellan RISE SICS och KTH för att utveckla ett nästa-generations distribuerat system kapabelt av CDA. Det är två problem som systemet syftar på att lösa: hårdvaruacceleration och beräkningsdelning. Det första handlar om hur BigData och maskininlärningssystem som sådan som TensorFlow, Pandas och Numpy måste kunna samarbeta så effektivt som möjligt. Hårdvaruacceleration relaterar till hur back-end delen i den dagens distribuerade beräknings system, såsom Spark och Flink, flaskhalsas av Javas Virtuella Maskin. JVM:en abstraherar över den underliggande hårvaran. Som resultat blir dess applikationer portabla, men ger också upp möjligheten att fullständigt utnyttja de tillgängliga hårdvaruresurserna. Den här avhandlingen siktar på att utforska området kring Domänspecifika Språk (DSLer) och kodgenerering som en lösning till hårdvaruacceleration. Idén är att översätta inkommande förfrågningar till låg-nivå kod, skräddarsydd till varje arbetar maskin’s specifika hårdvara. Till detta ändamål har två Scala DSLer utvecklats för generering av Rust kod. Rust är ett nytt låg-nivå språk med ett unikt vidtagande kring minneshantering som gör det både lika säkert som Java och snabbt som C. Scala är ett språk som passar bra tillutveckling av DSLer pågrund av dess flexibla syntax och semantik. Den första DSLen är implementerad som en sträng-interpolator. Interpolatorn sammanfogar strängar av Rust kod, under kompileringstid eller exekveringstid, och passerar resultatet till enextern process för statisk kontroll. Den andra DSLen består istället av ett API för att konstruera ett abstrakt syntaxträd, som efteråt kan traverseras och skrivas ut till Rust kod. API:et kombinerar tre koncept: heterogena listor, flytande gränssnitt, och algebraiska datatyper. Dessa tillåter användaren att uttrycka avancerad Rust syntax, såsom polymorfiska strukts, funktioner, och traits, utan att uppoffra typsäkerhet.

This thesis presents the design and implementation of an extension of the self-hosted Miking compiler to enable the generation of JavaScript code for different runtime environments and web browsers. Miking is a framework for developing domain-specific and general-purpose programming languages through sound language fragment composition, among other things, to create efficient compilers. Miking Core encapsulates a meta-language called Miking Lang and a fundamental functional Miking Expression language which Miking Lang itself is also lowered to. The presented backend translates Miking expressions into semantically equivalent effective, readable, sound, and correct JavaScript programs. In this report, development challenges, implementation methods, and techniques are also discussed and evaluated along with a review of the final compiler backend. Likewise, details on JavaScript-specific optimizations and pattern-matching compilation are presented, including how tail recursion is handled to enable complex Miking programs to be compiled into flexible and efficient JavaScript. / Detta examensarbete presenterar design och implementation för utveckling av Miking-kompilatorn, med syfte att möjliggöra generering av JavaScript-kod för olika exekveringsmiljöer och webbläsare. Miking är ett ramverk för att utveckla domänspecifika och generella programmeringsspråk genom sund komposition av språksfragment som kan används för att skapa effektiva kompilatorer. Miking Core ramverket innehåller ett metaspråk kallat Miking Lang, vilket ”sänks” till det mer grundläggande funktionella Miking Expression-språket. ”Sänkning” betyder i huvudsak att skriva om mer komplexa semantiska konstruktioner i form av enklare. Den backend som presenteras översätter Miking-uttryck till semantiskt ekvivalenta JavaScript program som också är effektiva, läsbara, sunda och korrekta. I denna rapport diskuteras och utvärderas även utvecklingsutmaningar, implementeringsmetod och andra tekniker som har använts under arbetet. På samma sätt presenteras detaljer om JavaScript-specifika optimeringar och mönstermatchningskompilering, inklusive hur svansrekursion hanteras för att möjliggöra kompilering av komplexa Miking-program till flexibel och effektiv JavaScript med hjälp av ”trampoline” teknik.

No description available.

Hardware-software co-design techniques are very suitable to develop the next generation of sensornet applications, which have high computational demands. By making use of a low power FPGA, the peak computational performance of a sensor node can be improved without significant degradation of the standby power dissipation. In this contribution, we present a methodology and tool to enable hardware/software co-design for sensor node application development. We present the integration of nesC, a sensornet programming language, with GEZEL, an easy-to-use hardware description language. We describe the hardware/software interface at different levels of abstraction: at the level of the design language, at the level of the co-simulator, and in the hardware implementation. We use a layered, uniform approach that is particularly suited to deal with the heterogeneous interfaces typically found on small embedded processors. We illustrate the strengths of our approach by means of a prototype application: the integration of a hardware-accelerated crypto-application in a nesC application. / Master of Science