FRAMEWORK SYNTHESIS FOR SYMBOLIC EXECUTION OF EVENT-DRIVEN FRAMEWORKS

Symbolic execution is a powerful program analysis technique, but it is very challenging to apply to programs built using event-driven frameworks, such as Android. The main reason is that the framework code itself is too complex to symbolically execute. The standard solution is to manually create a framework model that is simpler and more amenable to symbolic execution. However, developing and maintaining such a model by hand is difficult and error-prone. We claim that we can leverage program synthesis to introduce a high-degree of automation to the process of framework modeling. To support this thesis, we present three pieces of work. First, we introduced SymDroid, a symbolic executor for Android. While Android apps are written in Java, they are compiled to Dalvik bytecode format. Instead of analyzing an app’s Java source, which may not be available, or decompiling from Dalvik back to Java, which requires significant engineering effort and introduces yet another source of potential bugs in an analysis, SymDroid works directly on Dalvik bytecode. Second, we introduced Pasket, a new system that takes a first step toward automatically generating Java framework models to support symbolic execution. Pasket takes as input the framework API and tutorial programs that exercise the framework. From these artifacts and Pasket's internal knowledge of design patterns, Pasket synthesizes an executable framework model by instantiating design patterns, such that the behavior of a synthesized model on the tutorial programs matches that of the original framework. Lastly, in order to scale program synthesis to framework models, we devised adaptive concretization, a novel program synthesis algorithm that combines the best of the two major synthesis strategies: symbolic search, i.e., using SAT or SMT solvers, and explicit search, e.g., stochastic enumeration of possible solutions. Adaptive concretization parallelizes multiple sub-synthesis problems by partially concretizing highly influential unknowns in the original synthesis problem. Thanks to adaptive concretization, Pasket can generate a large-scale model, e.g., thousands lines of code. In addition, we have used an Android model synthesized by Pasket and found that the model is sufficient to allow SymDroid to execute a range of apps.

Klasseneffekte oder individuelle Einflussgrößen. Was bestimmt die Teilnahme am Instrumentallernen im Grundschulalter

In den vergangenen Jahren hat die Diskussion um kulturelle Teilhabe im Rahmen der Ergebnisse großer Bildungsstudien zugenommen. Diese hatten eine hochgradige Abhängigkeit des Bildungserfolgs und des Kompetenzerwerbs vom sozialen Hintergrund der Kinder und ihrer Familien konstatiert (u.a. Ehmke & Jude 2010, S. 250). Auch für den Teilaspekt der kulturellen Teilhabe ließen sich in Studien soziale Disparitäten feststellen: Die rezeptive Nutzung kultureller Angebote durch Kinder und Jugendliche unterliegt einer deutlichen sozialen Selektivität (Autorengruppe Bildungsberichterstattung 2012, S. 165). Gleichzeitig ist mit dem Programm Jedem Kind ein Instrument eine große Initiative zur Förderung frühen Instrumentallernens in der Grundschulzeit angelaufen. Die Initiatoren verfolgen dabei explizit das Ziel, die Kluft „zwischen kulturaffinen Elternhäusern und bildungsfernen Schichten" (Kulturstiftung des Bundes, 2012) in Bezug auf kulturelle Bildung zu verringern, eine „Grundversorgung" (ebd.) sicherzustellen und im demokratischen Sinne niemanden von der Alphabetisierung in Sachen Kunst auszuschließen (Völckers, 2007). Die Teilnahme von Kindern an Instrumentalunterricht während der Grundschulzeit wird hier also als ein Aspekt aktiver kultureller Teilhabe gedeutet und wird im Folgenden einer Analyse unterzogen. (DIPF/Orig.)

Herausforderung Inklusion? Ein mehrperspektivischer Blick auf die JeKi-Praxis an Schulen mit gemeinsamem Unterricht (GU)

[Der Beitrag nähert sich der Frage], ob die aktuelle JeKi-Praxis günstige Voraussetzungen für die erweiterte Einführung inklusiver Settings bietet und wie die bestehenden Ansätze eines inklusiven JeKi-Unterrichts in Grundschulen mit gemeinsamem Unterricht eingeschätzt werden können. [...] Für jede dieser Ebenen wurden in der Studie „JeKi und gemeinsamer Unterricht" ausgewählte Fragestellungen untersucht, in der vorliegenden Darstellung sollen zwei Aspekte im Vordergrund stehen, die der innerpsychischen und der institutionellen Ebene zugeordnet werden können. (DIPF/Orig.)

Articulation in property programs : an international multi-campus tertiary model

This paper will present program developers and institutional administrators with a program delivery model suitable for cross cultural international delivery developing students from industry through to master’s level tertiary qualifications. The model was designed to meet the needs of property professionals from an industry where technical qualifications are the norm and tertiary qualifications are emerging. A further need was to develop and deliver a program that enhanced the University’s current program profile in both the domestic and international arenas. Early identification of international educational partners, industry need and the ability to service the program were vital to the successful development of Master of Property program. The educational foundations of the program rest in educational partners, local tutorial support, international course management, cultural awareness of and in content, online communication fora, with a delivery focus on problem-based learning, self-directed study, teamwork and the development of a global understanding and awareness of the international property markets. In enrolling students from a diverse cultural background with technical qualifications and/or extensive work experience there are a number of educational barriers to be overcome for all students to successfully progress and complete the program. These barriers disappear when the following mechanisms are employed: individual student pathways, tutorial support by qualified peers, enculturation into tertiary practice, assessment tasks that recognise cultural norms and values, and finally that value is placed on the experiential knowledge, cultural practices and belief systems of the students.

Educação Tutorial como ferramenta no Ensino-Aprendizagem de Audiovisual

This paper aims to highlight the importance of Tutorial Education Program (TEP) for undergraduate courses in conjunction with the graduate programs, highlighting the relevance of the triad teaching, research and extension activities also present in the TEP Interdisciplinary in Radio and Television from the FAAC/UNESP.

A tutorial on program development and optimization using the Ciao preprocessor

We present in a tutorial fashion CiaoPP, the preprocessor of the Ciao multi-paradigm programming system, which implements a novel program development framework which uses abstract interpretation as a fundamental tool. The framework uses modular, incremental abstract interpretation to obtain information about the program. This information is used to validate programs, to detect bugs with respect to partial specifications written using assertions (in the program itself and/or in system libraries), to generate and simplify run-time tests, and to perform high-level program transformations such as multiple abstract specialization, parallelization, and resource usage control, all in a provably correct way. In the case of validation and debugging, the assertions can refer to a variety of program points such as procedure entry, procedure exit, points within procedures, or global computations. The system can reason with much richer information than, for example, traditional types. This includes data structure shape (including pointer sharing), bounds on data structure sizes, and other operational variable instantiation properties, as well as procedure-level properties such as determinacy, termination, non-failure, and bounds on resource consumption (time or space cost).

Proof Methods for Corecursive Programs

Recursion is a well-known and powerful programming technique, with a wide variety of applications. The dual technique of corecursion is less well-known, but is increasingly proving to be just as useful. This article is a tutorial on the four main methods for proving properties of corecursive programs: fixpoint induction, the approximation (or take) lemma, coinduction, and fusion.