Search

Objective: To investigate the oncological safety and potential cost savings of selective histopathological examination after appendectomy. Background: The necessity of routine histopathological examination after appendectomy has been questioned, but prospective studies investigating the safety of a selective policy are lacking. Methods: In this multicenter, prospective, cross-sectional study, inspection and palpation of the (meso)appendix was performed by the surgeon in patients with suspected appendicitis. The surgeon's opinion on additional value of histopathological examination was reported before sending all specimens to the pathologist. Main outcomes were the number of hypothetically missed appendiceal neoplasms with clinical consequences benefiting the patient (upper limit two-sided 95% confidence interval below 3:1000 considered oncologically safe) and potential cost savings after selective histopathological examination. Results: Seven thousand three hundred thirty-nine patients were included. After a selective policy, 4966/7339 (67.7%) specimens would have been refrained from histopathological examination. Appendiceal neoplasms with clinical consequences would have been missed in 22/4966 patients. In 5/22, residual disease was completely resected during additional surgery. Hence, an appendiceal neoplasm with clinical consequences benefiting the patient would have been missed in 1.01:1000 patients (upper limit 95% confidence interval 1.61:1000). In contrast, twice as many patients (10/22) would not have been exposed to potential harm due to re-resections without clear benefit, whereas consequences were neither beneficial nor harmful in the remaining seven. Estimated cost savings established by replacing routine for selective histopathological examination were 725,400 per 10,000 patients. Conclusions: Selective histopathological examination after appendectomy for suspected appendicitis is oncologically safe and will likely result in a reduction of pathologists' workload, less costs, and fewer re-resections without clear benefit.

We present FoxDec: an approach to C code decompilation that aims at producing sound and recompilable code. Formal methods are used during three phases of the decompilation process: control flow recovery, symbolic execution, and variable analysis. The use of formal methods minimizes the trusted code base and ensures soundness: the extracted C code behaves the same as the original binary. Soundness and recompilablity enable C code decompilation to be used in the contexts of binary patching, binary porting, binary analysis and binary improvement, with confidence that the recompiled code’s behavior is consistent with the original program. We demonstrate that FoxDec can be used to improve execution speed by recompiling a binary with different compiler options, to patch a memory leak with a code transformation tool, and to port a binary to a different architecture. FoxDec can also be leveraged to port a binary to run as a unikernel, a minimal and secure virtual machine usually requiring source access for porting.

As AI systems increasingly pervade modern society and lead to manifold and diverse consequences, the development of internationally recognized and industry-specific frameworks focusing on legal and ethical principles is crucial. This report aims at (a) understanding how the 7 Key Requirements for Trustworthy AI impact the Media and Technology sector (MTS) and at (b) putting forward guidelines to ensure compliance with the 7 Key Requirements. The report identifies four application areas of AI MTS, i.e. automating data capture and processing, automating content generation, automating content mediation and automating communication. Subsequently, the 7 Key Requirements are discussed within each of the four identified themes. Ultimately, recommendations are made to ensure that AI development and adoption in Media and Technology sector is compliant with the 7 Key Requirements. Three clusters of recommendations are proposed: (1) addressing data power and positive obligations, (2) empowerment by design and risk assessments and (3) cooperative responsibility and stakeholder engagements.

We present a methodology for generating a characterization of the memory used by an assembly program, as well as a formal proof that the assembly is bounded to the generated memory regions. A formal proof of memory usage is required for compositional reasoning over assembly programs. Moreover, it can be used to prove low-level security properties, such as integrity of the return address of a function. Our verification method is based on interactive theorem proving, but provides automation by generating pre- and postconditions, invariants, control-flow, and assumptions on memory layout. As a case study, three binaries of the Xen hypervisor are disassembled. These binaries are the result of a complex build-chain compiling production code, and contain various complex and nested loops, large and compound data structures, and functions with over 100 basic blocks. The methodology has been successfully applied to 251 functions, covering 12,252 assembly instructions.

Thuiszitters Het aantal leerlingen dat langer dan drie maanden thuiszit en niet naar school gaat – ‘thuiszitters’ – stijgt. Een stijging die we al jaren zien en die doorzet, ondanks de inspanningen die voortvloeien uit het Thuiszitterspact (2016) of Passend onderwijs (2014). Vanuit de onderwijspraktijk wordt de omgang met leerlingen met gedragsproblemen als moeilijk ervaren en in verband gebracht met het aantal thuiszitters dat niet terugloopt maar zelfs oploopt. Het Nationaal Regieorgaan Onderwijsonderzoek (NRO) heeft in 2017 daarom subsidie beschikbaar gesteld voor praktijkgericht onderzoek naar gedrag en (passend) onderwijs: ‘Leraren, in primair en voortgezet onderwijs, vinden passend onderwijs vaak een belasting. Vooral de omgang met en aanpak van leerlingen met probleemgedrag vinden zij moeilijk’ (NRO, 2017). Aannames uit literatuur Op basis van de empirische wetenschappelijke literatuur was de verwachting vooraf dat achter de thuiszittersproblematiek gedragsproblemen schuilgaan; die samenhangen met moeilijk hanteerbaar gedrag op school en in de klas; dat jongens hierin een groter aandeel hebben dan meisjes; dat ze onvoldoende gemotiveerd zijn voor school; dat hun cognitieve capaciteiten tekortschieten; dat er meer schoolwisselingen plaatsvinden op grond hiervan; dat er vaker een negatief schooladvies ligt bij de transfer naar het voortgezette onderwijs. Voorts werd aangenomen; dat het bij hen thuis ontbreekt aan een voldoende mate van ouderbetrokkenheid en sociaal kapitaal; dat zij uit een economisch gedepriveerde achtergrond komen (lage SES); dat de sociale cohesie op school voor hen tekortschiet of dat zij deze verstoren; dat zij vaker dan andere leerlingen te maken hebben met justitiële maatregelen; dat zij vaker uit stedelijke gebieden komen; dat cultuur een rol speelt, en dat de laatste school vaker een focusschool is ( uitsluitend vmbo in plaats van diversiteit in typen onderwijs). Wat uit onze meervoudige casestudy blijkt Een aantal aannames zoals hiervoor genoemd is in ons onderzoek niet bevestigd. Wij vonden voor de zuiver externaliserende gedragsproblematiek (oppositioneel en opstandig) geen hogere (maar zelfs lagere) kans op thuiszitten; juist voor meisjes een licht hogere kans op thuiszitten; voor internaliserende gedragsproblematiek een hogere kans op thuiszitten, en geen indicaties dat een gebrek aan schoolmotivatie of cognitieve problemen bepalend zijn voor thuiszitten. Ook vonden wij dat ouderbetrokkenheid en sociaal kapitaal als termen niet weergeven wat thuis speelt (uit onze analyse komen ‘relatieproblemen tussen ouders’, ‘gescheiden ouders’, ‘problemen met loyaliteit van kind naar ouder’ en ‘geen contact met een ouder’ naar voren; uit de interviews met leerlingen wordt dit verder ingekleurd met overbelasting van ouders, overmatige stress of ernstige problemen thuis); dat vaker gebukt gaan onder justitiële maatregelen wel naar voren komt, maar bij thuiszitters met name in civielrechtelijke zin, zoals politiecontacten vanuit een beschermend optreden (i.v.m. weglopen, vermissing en opsporen) of gesloten plaatsingen en specialistische hulp (zoals jeugdzorg plus, GGZ hulp). Concluderend Concluderend kunnen wij stellen dat het belangrijk is dat scholen (nog) meer aandacht hebben voor de persoon en omstandigheden achter de leerling. Dat zij gedrag (waaronder verzuim) zien als een signaal voor tijdige interventie, ook op of via school, in plaats van een ‘automatische’ indicatie voor voortgezet speciaal onderwijs of het plaatsen op een lager onderwijsniveau.

Contains fulltext : 132833.pdf (Author’s version postprint ) (Open Access)

3D-NoC has emerged to provide fast and power efficient connection between the layers of 2D-NoCs using Through-Silicon-Vias (TSV). Thermal stress, warpage, impurities and misalignment during the manufacturing process make these expensive TSVs vulnerable to faults. Chips with faulty TSVs should be either discarded or utilized by providing a proper fault-tolerant method. In this paper, we target designing a reconfigurable fault-tolerant routing algorithm capable of tolerating fabrication-time or run-time TSV failures. The proposed algorithm ensures a fault-free communication between any two nodes in the presence of TSV failures. Experimental results show that the proposed fault-tolerant routing algorithm provides 100% reliability as long as there is one healthy TSV in the eastmost or westmost column. The reliability of the counterpart algorithm, the Elevator-first routing algorithm, drops to 75% and 45% in presence of one and two faulty TSVs, respectively.

Deadlock detection is a challenging issue in the analysis and design of on-chip networks. We have designed an algorithm to detect deadlocks automatically in on-chip networks with wormhole switching. The algorithm has been specified and proven correct in ACL2. To enable a top-down proof methodology, some parts of the algorithm have been left unimplemented. For these parts, the ACL2 specification contains constrained functions introduced with defun-sk. We used single-threaded objects to represent the data structures used by the algorithm. In this paper, we present details on the proof of correctness of the algorithm. The process of formal verification was crucial to get the algorithm flawless. Our ultimate objective is to have an efficient executable, and formally proven correct implementation of the algorithm running in ACL2., In Proceedings ACL2 2011, arXiv:1110.4473

PikeOS is an industrial operating system for safety and security critical applications in, for example, avionics and automotive contexts. A consortium of several European partners from industry and academia works on the certification of PikeOS up to at least Common Criteria EAL5+, with "+" being applying formal methods compliant up to EAL7. We have formalized the hardware independent security-relevant part of PikeOS that is to be used in a certification context. Over this model, intransitive noninterference has been proven. We present the model and the methodology used to create the model. All results have been formalized in the Isabelle/HOL theorem prover.

De Ad staat (opnieuw) op een kruispunt. Dat is de conclusie van het onderzoek dat SEO economisch onderzoek met haar partners ecbo, ROA en Kohnstamm Instituut heeft gedaan naar het verloop van de uitrol van de Associate degree sinds de definitieve wettelijke verankering. Het definitief wettelijk verankeren van de Ad heeft er niet toe geleid dat het aantal Ad-programma's en de instroom van studenten de afgelopen jaren een vlucht heeft genomen. Belangrijke verklaring voor de stagnatie is dat het pas sinds augustus 2014 weer mogelijk is aanvragen voor nieuwe Ad-programma's in te dienen. Toch lijkt het te eenvoudig om daar de gehele oorzaak te zoeken. De Ad lijkt zich de afgelopen jaren te bevinden in een vicieuze cirkel rondom het centrale punt van onbekendheid bij (veel van) de betrokkenen en een (daaruit voortvloeiende of daarvoor verklarende) onduidelijke positie in het onderwijsstelsel en op de arbeidsmarkt. Daartegenover staat dat sommige instellingen en specifieke Ad-programma's veel studenten weten te trekken, waarvan een relatief groot aandeel afstudeert. Ook zijn werkgevers en studenten die de Ad kennen overwegend positief en komen er momenteel positieve signalen vanuit beleidsmakers en onderwijsinstellingen. Daarmee staat de Ad op een kruispunt. De Ad lijkt meerwaarde te hebben, maar mag dat nu gaan bewijzen met steun van alle betrokkenen. De wettelijke verankering is geregeld en geïmplementeerd, nu kan de uitrol in de praktijk gaan plaatsvinden. Vandaar de titel van dit rapport: "klaar voor de groei?"

Om zicht te krijgen op de effecten van een brede invoering van een masteropleiding voor leraren, laat het ministerie van Onderwijs, Cultuur en Wetenschap onderzoek uitvoeren dat een theoretisch (wetenschappelijk) en empirisch (causaal) verband legt tussen de masteropleiding van leraren en de kwaliteit van het onderwijs. Dit rapport bevat daartoe een nulmeting waarin potentiële effecten worden geïdentificeerd, een onderzoeksdesign wordt ontworpen en een eerste meting wordt uitgevoerd. Mogelijke effecten van een masteropleiding op leraren en hun omgeving zijn geïdentificeerd aan de hand van een analyse van relevante beleidsdocumenten, een analyse van de relevante wetenschappelijke literatuur en door middel van 35 interviews met betrokkenen in het onderwijsveld. Effecten kunnen worden gemeten door uitkomstmaten te vergelijken tussen leraren met en zonder masteropleiding op verschillende momenten in de tijd (verschil-in-verschil meting). De onderzoekspopulatie wordt daarom opgebouwd uit een interventiegroep (leraren die een masteropleiding volgen) en een controlegroep (leraren zonder masteropleiding). Effecten kunnen pas na een vervolgmeting worden vastgesteld. De nulmeting heeft een goede basis gelegd voor het meten van effecten van een onderwijsmaster op hbo-niveau. Er zijn goed vergelijkbare interventie- en controlegroepen opgezet, die in de loop van de tijd gevolgd kunnen worden. Het vervolg-onderzoek is inmiddels van start gegaan en loopt tot 2017.

This paper reports our initial experiments with using external ATP on some corpora built with the ACL2 system. This is intended to provide the first estimate about the usefulness of such external reasoning and AI systems for solving ACL2 problems., In Proceedings ACL2 2014, arXiv:1406.1238

Intransitive noninterference has been a widely studied topic in the last few decades. Several well-established methodologies apply interactive theorem proving to formulate a noninterference theorem over abstract academic models. In joint work with several industrial and academic partners throughout Europe, we are helping in the certification process of PikeOS, an industrial separation kernel developed at SYSGO. In this process, established theories could not be applied. We present a new generic model of separation kernels and a new theory of intransitive noninterference. The model is rich in detail, making it suitable for formal verification of realistic and industrial systems such as PikeOS. Using a refinement-based theorem proving approach, we ensure that proofs remain manageable.

Contains fulltext : 130035.pdf (author's version ) (Open Access)

In modern chip architectures, the increase in parallelization brings about highly complex on-chip communication fabrics. We present WickedXmas, a tool that facilitates the design and formal verification of such interconnects. The tool is based on the language xMAS, which is a high level design language for communication fabrics, originally proposed by Intel. The use of xMAS ensures that many common modelling errors such as unintended loss of data or dangling wires are prevented by construction. Therefore, the major challenge in verifying xMAS models is establishing deadlock freedom. WickedXmas can automatically detect deadlocks or prove their absence. If a deadlock is found, it is presented to the user for further analysis. Experimental evaluation on a range of interconnects shows good performance and scalability of WickedXmas in contrast to verification from scratch, or using existing model checking techniques. Using WickedXmas, a user can draw a communication fabric and formally verify it automatically. Keywords: Communication Fabrics, Deadlock Detection, Formal Verification Tools

In the multi-core era, on-chip communication networks are key to system correctness and performance. To deal with their growing complexity, micro-architectural models capture the intent of architects and provide means for formal analysis. However, the analysis of such micro-architectural models is restricted to non-scalable and/or very specific approaches. We present a novel scalable approach to support the symbolic channel type inference of large micro-architectural models described in the xMAS language proposed by Intel. We define an algorithm that computes all possible messages that can occur in a communication channel, treating their payload symbolically. These results can be used for further analysis such as verifying absence of misrouting, deriving inductive invariants and deadlock detection. We illustrate our approach on a Spidergon network developed at STMicroelectronics.

In joint work with several industrial and academic partners throughout Europe, we are working towards the certification of PikeOS -- an industrial separation kernel developed at SYSGO -- according to the highest level of the Common Criteria. We present a new generic model of separation kernels that includes interrupts, control and context switches. For this generic model, noninterference has been proven in the Isabelle/HOL theorem prover from proof obligations on the step function. Noninterference holds for all separation kernels which satisfy these assumptions. In this paper, we discuss this methodology for certification purposes. On the one hand, it is clear that our instantiation of the step function for PikeOS must satisfy the proof obligations. On the other hand, there are many implicit assumptions made in defining the run function, that is, in defining how the step function is applied. Based on work-in-progress, we address the issue of providing evidence that PikeOS indeed satisfies our generic notion of noninterference.

We formally compare two industrially relevant and popular models of noninterference, namely, the model defined by Rushby and the one defined by Greve, Wilding, and Vanfleet (GWV). We create a mapping between the objects and relations of the two models. We prove a number of theorems showing under which assumptions a system identified as "secure" in one model is also identified as "secure" in the other model. Using two examples, we illustrate and discuss some of these assumptions. Our main conclusion is that the GWV model is more discriminating than the Rushby model. All systems satisfying GWV’s Separation also satisfy Rushby’s noninterference. The other direction only holds if we additionally assume that GWV systems are such that every partition is assigned at most one memory segment. All of our proofs have been checked using the Isabelle/HOL proof assistant. Keywords: Noninterference; information flow security; formal models

Contains fulltext : 135061.pdf (Author’s version preprint ) (Open Access) 2014 22ND INTERNATIONAL CONFERENCE ON VERY LARGE SCALE INTEGRATION (VLSI-SOC) : OCTOBER 6TH – 8TH, 2014 PLAYA DEL CARMEN, MEXICO : CONFERENCE PROCEEDINGS