Tracing just-in-time compilers (TJITs) determine frequently executed traces (hot paths and loops) at run time. These traces are then analyzed and optimized, and finally specialized machine code is generated. Up to now, TJITs employed standard compiler construction algorithms to analyze and optimize traces. We propose to leverage automated theorem provers to optimize traces at run time.
This artifact allows others to reproduce the results seen in this paper for MakeCode and CODAL, using the BBC micro:bit. The artifact contains an offline build environment for CODAL and MakeCode, allowing evaluators to test and build programs locally. In addition, we also provide espruino and micropython virtual machines to further increase repeatability of our results. Evaluators should download the virtual machine containing all pre-requisite tools, and use an oscilloscope to observe wave forms (used for timing) generated by the micro:bit, and a serial terminal to observe results reported from the micro:bit over serial. Full documentation is available at: https://lancaster-university.github.io/lctes-artefact-evaluation/
We are experiencing a technology shift: Powerful and easy-to-use touchscreen-based mobile devices like smartphones and tablets are becoming more prevalent than traditional PCs and laptops. We propose that computer programming, and thus teaching of programming, can and should be done directly on the mobile devices themselves, without the need for a separate PC or laptop to write code. In this workshop, participants will learn about developing software directly on smartphones without a PC using TouchDevelop, a novel application creation environment on Windows Phone 7 from Microsoft Research (http://touchdevelop.com). Its typed, structured programming language is built around the idea of only using a touchscreen as the input device to author code. A semi-structured code editor makes it easy to navigate between different syntax elements. By inferring types and mining previously written programs, the editor provides highly predictive auto-completion suggestions to the user. The language provides built-in primitives that make it easy to access the rich sensor data available on a mobile device. Programming on mobile devices engages students in new ways, allowing them to access and manipulate programmatically their most personal digital data such as pictures, videos, and music. Programming on smartphones which we carry around with us at all times means instant gratification for students, as they can show their games and applications to their friends, and it means that students can do their homework or additional practicing at all times. For this workshop, a laptop is optional; Windows Phone 7 devices will be provided for exercises.
From paper to computers, the way that we have been writing down thoughts and performing symbolic computations has been constantly evolving. Teaching methods closely follow this trend, leveraging existing technology to make teaching more effective and preparing students for their later careers with the available technology. Right now, in 2012, we are in the middle of another technology shift: instead of using PCs and laptops, mobile devices are becoming more prevalent for most everyday computing tasks. In fact, never before in human history were incredibly powerful and versatile computing devices such as smartphones available and adopted so broadly. We propose that computer programming, and thus the teaching of programming, can and should be done directly on the mobile devices themselves, without the need for a separate PC or laptop to write code. Programming on smartphones that we carry around with us at all times means instant gratification for students, as they can show their games and applications to their friends, and it means that students can do their homework or additional practicing at all times. We describe TouchDevelop, a novel mobile programming environment, and call out challenges that need to be overcome and opportunities that it creates.
Physical computing involves the creation of interactive digital devices that sense and respond to the world around them [1]. Typically, sensors, actuators and communications modules are connected to a microcontroller (MCU) running code that maps sensed inputs into outputs such as lighting, sound and electro-mechanical actuation [7]. This prototyping process builds on a wide range of disciplines including electronics, mechatronics, computer science and software development. It's typically experimental, creative and highly iterative.
We give a case study for a Satisfiability Modulo Theories (SMT) solver usage in functional verification of a real world operating system. In particular, we present a view of the E-matching pattern annotations on quantified formulas as a kind of logic programming language, used to encode semantics of the programming language undergoing verification. We postulate a few encoding patterns to be benchmark problems for a possible E-matching alternative. We also describe features required from the SMT solver in deductive software verification scenarios.
'%3e%3cpath fill='%23012169' d='M0 0v30h60V0z'/%3e%3cpath stroke='%23fff' stroke-width='6' d='m0 0 60 30m0-30L0 30'/%3e%3cpath stroke='%23C8102E' stroke-width='4' d='m0 0 60 30m0-30L0 30' clip-path='url(%23b)'/%3e%3cpath stroke='%23fff' stroke-width='10' d='M30 0v30M0 15h60'/%3e%3cpath stroke='%23C8102E' stroke-width='6' d='M30 0v30M0 15h60'/%3e%3c/g%3e%3c/svg%3e)
'%3e%3ccircle r='20' fill='%23008'/%3e%3ccircle r='17.5' fill='%23fff'/%3e%3ccircle r='3.5' fill='%23008'/%3e%3cg id='d'%3e%3cg id='c'%3e%3cg id='b'%3e%3cg id='a' fill='%23008'%3e%3ccircle r='.875' transform='rotate(7.5 -8.75 133.5)'/%3e%3cpath d='M0 17.5.6 7 0 2l-.6 5L0 17.5z'/%3e%3c/g%3e%3cuse xlink:href='%23a' transform='rotate(15)'/%3e%3c/g%3e%3cuse xlink:href='%23b' transform='rotate(30)'/%3e%3c/g%3e%3cuse xlink:href='%23c' transform='rotate(60)'/%3e%3c/g%3e%3cuse xlink:href='%23d' transform='rotate(120)'/%3e%3cuse xlink:href='%23d' transform='rotate(-120)'/%3e%3c/g%3e%3c/svg%3e)
