Change search
Refine search result
1 - 39 of 39
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1.
    Artho, Cyrille
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Ölveczky, P.C.
    Formal Techniques for Safety-Critical Systems (FTSCS 2015)2018In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 154, p. 1-2Article in journal (Refereed)
  • 2.
    Austrin, Per
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Kaski, Petteri
    Koivisto, Mikko
    Nederlof, Jesper
    Sharper Upper Bounds for Unbalanced Uniquely Decodable Code Pairs2018In: IEEE Transactions on Information Theory, ISSN 0018-9448, E-ISSN 1557-9654, Vol. 64, no 2, p. 1368-1373Article in journal (Refereed)
    Abstract [en]

    Two sets of 0-1 vectors of fixed length form a uniquely decodeable code pair if their Cartesian product is of the same size as their sumset, where the addition is pointwise over integers. For the size of the sumset of such a pair, van Tilborg has given an upper bound in the general case. Urbanke and Li, and later Ordentlich and Shayevitz, have given better bounds in the unbalanced case, that is, when either of the two sets is sufficiently large. Improvements to the latter bounds are presented.

  • 3.
    Berglund, Lasse
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Executive Summaries in Software Model Checking2018Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    Model checking is a technique used to verify whether a model meets a given specification by exhaustively and automatically checking each reachable state in the model. It is a well-developed technique, but it suffers from some issues, perhaps most importantly the state space explosion problem. Models may contain so many states that must be checked means that the model checking procedure may be intractable. In this thesis we investigate whether procedure summaries can be used to improve the performance of model checking. Procedure summaries are concise representations of parts of a program, such as a function or method. We present a design and an implementation of dynamically generated summaries as an extension of Java PathFinder, a virtual machine executing Java bytecode that is able to model check programs written in Java by backtracking execution, to explore different schedulings etc. We find that our summaries incur an overhead that outweighs the benefits in most cases, but the approach shows promise in certain cases, in particular when stateless model checking is used. We also provide some statistics related to cases when our summaries are applicable that could provide guidance for future work within this field.

  • 4. Bhattacharya, S.
    et al.
    Chakrabarty, D.
    Henzinger, M.
    Na Nongkai, Danupon
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Dynamic algorithms for graph coloring2018In: Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, Association for Computing Machinery , 2018, p. 1-20Conference paper (Refereed)
    Abstract [en]

    We design fast dynamic algorithms for proper vertex and edge colorings in a graph undergoing edge insertions and deletions. In the static setting, there are simple linear time algorithms for ( δ + 1)vertex coloring and (2 δ 1)edge coloring in a graph with maximum degree δ. It is natural to ask if we can efficiently maintain such colorings in the dynamic setting as well. We get the following three results. (1) We present a randomized algorithm which maintains a ( δ+1)-vertex coloring with O(log δ) expected amortized update time. (2) We present a deterministic algorithm which maintains a (1 + o(1)) δ-vertex coloring with O(polylog δ) amortized update time. (3) We present a simple, deterministic algorithm which maintains a (2 δ)edge coloring with O(log δ) worst-case update time. This improves the recent O( δ)-edge coloring algorithm with Õ ( p δ) worst-case update time [4]. 

  • 5.
    Bhattacharya, Sayan
    et al.
    University of Warwick, UK.
    Na Nongkai, Danupon
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Saranurak, Thatchaphol
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Nondeterminism and Completeness for Dynamic AlgorithmsManuscript (preprint) (Other academic)
  • 6.
    Bilardi, Gianfranco
    et al.
    Univ Padua, Dept Informat Engn, I-35131 Padua, Italy..
    Scquizzato, Michele
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS. Univ Padua, Padua, Italy.
    Silvestri, Francesco
    Univ Padua, Dept Informat Engn, I-35131 Padua, Italy..
    A Lower Bound Technique for Communication in BSP2018In: ACM TRANSACTIONS ON PARALLEL COMPUTING, ISSN 2329-4949, Vol. 4, no 3, article id UNSP 14Article in journal (Refereed)
    Abstract [en]

    Communication is a major factor determining the performance of algorithms on current computing systems; it is therefore valuable to provide tight lower bounds on the communication complexity of computations. This article presents a lower bound technique for the communication complexity in the bulk-synchronous parallel (BSP) model of a given class of DAG computations. The derived bound is expressed in terms of the switching potential of a DAG, that is, the number of permutations that the DAG can realize when viewed as a switching network. The proposed technique yields tight lower bounds for the fast Fourier transform (FFT), and for any sorting and permutation network. A stronger bound is also derived for the periodic balanced sorting network, by applying this technique to suitable subnetworks. Finally, we demonstrate that the switching potential captures communication requirements even in computational models different from BSP, such as the I/O model and the LPRAM.

  • 7.
    Bosk, Daniel
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Rodríguez-Cano, Guillermo
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Greschbach, Benjamin
    KTH.
    Buchegger, Sonja
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Applying privacy-enhancing technologies: One alternative future of protests2018In: Protests in the Information Age: Social Movements, Digital Practices and Surveillance, Taylor & Francis, 2018, p. 73-94Chapter in book (Refereed)
    Abstract [en]

    While current technologies, such as online social networks, can facilitate coordination and communication for protest organization, they can also endanger political activists when the control over their data is ceded to third parties. For technology to be useful for activism, it needs to be trustworthy and protect the users’ privacy; only then can it be viewed as a potential improvement over more traditional, offline methods. Here, we discuss a selection of such privacy-enhancing technologies from a Computer Science perspective in an effort to open a dialogue and elicit input from other perspectives.

  • 8. Buss, S.
    et al.
    Itsykson, D.
    Knop, A.
    Sokolov, Dmitry
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Reordering rule makes OBDD proof systems stronger2018In: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2018, p. 161-1624Conference paper (Refereed)
    Abstract [en]

    Atserias, Kolaitis, and Vardi showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(∧, weakening), simulates CP∗ (Cutting Planes with unary coefficients). We show that OBDD(∧, weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring tautologies have polynomial size proofs in the OBDD(∧, weakening) system. The reordering rule allows changing the variable order for OBDDs. We show that OBDD (∧, weakening, reordering) is strictly stronger than OBDD(∧, weakening). This is proved using the Clique-Coloring tautologies, and by transforming tautologies using coded permutations and orification. We also give CNF formulas which have polynomial size OBDD(∧) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolve an open question proposed by Groote and Zantema. Applying dag-like and tree-like lifting techniques to the mentioned results, we completely analyze which of the systems among CP∗, OBDD(∧), OBDD(∧, reordering), OBDD(∧, weakening) and OBDD (∧, weakening, reordering) polynomially simulate each other. For dag-like proof systems, some of our separations are quasipolynomial and some are exponential; for tree-like systems, all of our separations are exponential.

  • 9. Danglot, Benjamin
    et al.
    Preux, Philippe
    Baudry, Benoit
    Monperrus, Martin
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Correctness attraction: a study of stability of software behavior under runtime perturbation2018In: Journal of Empirical Software Engineering, ISSN 1382-3256, E-ISSN 1573-7616, Vol. 23, no 4, p. 2086-2119Article in journal (Refereed)
    Abstract [en]

    Can the execution of software be perturbed without breaking the correctness of the output? In this paper, we devise a protocol to answer this question from a novel perspective. In an experimental study, we observe that many perturbations do not break the correctness in ten subject programs. We call this phenomenon “correctness attraction”. The uniqueness of this protocol is that it considers a systematic exploration of the perturbation space as well as perfect oracles to determine the correctness of the output. To this extent, our findings on the stability of software under execution perturbations have a level of validity that has never been reported before in the scarce related work. A qualitative manual analysis enables us to set up the first taxonomy ever of the reasons behind correctness attraction.

  • 10.
    Durieux, Thomas
    et al.
    Univ Lille, Lille, France.;INRIA, Le Chesnay, France..
    Hamadi, Youssef
    Ecole Polytech, Palaiseau, France..
    Yu, Zhongxing
    Univ Lille, Lille, France.;INRIA, Le Chesnay, France..
    Baudry, Benoit
    KTH, School of Electrical Engineering and Computer Science (EECS), Software and Computer systems, SCS.
    Monperrus, Martin
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Exhaustive Exploration of the Failure-oblivious Computing Search Space2018In: 2018 IEEE 11TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST), IEEE Press, 2018, p. 139-149Conference paper (Refereed)
    Abstract [en]

    High-availability of software systems requires automated handling of crashes in presence of errors. Failure-oblivious computing is one technique that aims to achieve high availability. We note that failure-obliviousness has not been studied in depth yet, and there is very few study that helps understand why failure-oblivious techniques work. In order to make failure-oblivious computing to have an impact in practice, we need to deeply understand failure-oblivious behaviors in software. In this paper, we study, design and perform an experiment that analyzes the size and the diversity of the failure-oblivious behaviors. Our experiment consists of exhaustively computing the search space of 16 field failures of large-scale open-source Java software. The outcome of this experiment is a much better understanding of what really happens when failure-oblivious computing is used, and this opens new promising research directions.

  • 11.
    Elffers, Jan
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Giráldez-Cru, Jakob
    KTH.
    Nordström, Jakob
    KTH.
    Vinyals, M.
    Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers2018In: 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Springer, 2018, Vol. 10929, p. 75-93Conference paper (Refereed)
    Abstract [en]

    We study cdcl-cuttingplanes, Open-WBO, and Sat4j, three successful solvers from the Pseudo-Boolean Competition 2016, and evaluate them by performing experiments on crafted benchmarks designed to be trivial for the cutting planes (CP) proof system underlying pseudo-Boolean (PB) proof search but yet potentially tricky for PB solvers. Our experiments demonstrate severe shortcomings in state-of-the-art PB solving techniques. Although our benchmarks have linear-size tree-like CP proofs, and are thus extremely easy in theory, the solvers often perform quite badly even for very small instances. We believe this shows that solvers need to employ stronger rules of cutting planes reasoning. Even some instances that lack not only Boolean but also real-valued solutions are very hard in practice, which indicates that PB solvers need to get better not only at Boolean reasoning but also at linear programming. Taken together, our results point to several crucial challenges to be overcome in the quest for more efficient pseudo-Boolean solvers, and we expect that a further study of our benchmarks could shed more light on the potential and limitations of current state-of-the-art PB solving.

  • 12.
    Gedin, Emanuel
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Hardness of showing hardness of the minimum circuit size problem2018Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    The problem of finding the smallest size of a circuit that computes a given boolean function, usually referred to as the minimum circuit size problem (MCSP), has been studied for many years but it is still unknown whether or not the problem is NP-hard. With this in mind we study properties of potential reductions to this problem. The reductions in focus are local natural reductions which has been common in other well-known proofs of NP-hardness. We present a generalized method that shows the existence of an algorithm solving any problem which has a local natural reduction to MCSP. In particular we show that if the decision problem of distinguishing satisfiable 3-SAT instances from those where at most 7/8 + o(1) of the clauses can be satisfied has a reduction to MCSP where any arbitrary bit of the output can be computed in O(n1 - ε) time for any ε > 0 then k-SAT can be solved by a circuit of depth 3 and size 2o(n).

  • 13.
    Glassey, Richard
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Haller, Philipp
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Wiggberg, Mattias
    KTH, School of Industrial Engineering and Management (ITM), Industrial Economics and Management (Dept.), Industrial Management.
    Agile and adaptive learning via the ECK-model in the software development academy2018In: CEUR Workshop Proceedings, CEUR-WS , 2018, Vol. 2193Conference paper (Refereed)
    Abstract [en]

    This paper reports the learning management experiences within an intensive three-month education that helps newly arrived in Sweden find work as IT professionals. The creation of the Software Development Academy was motivated by the migration crisis and the wider need to help integrate newcomers into the social and professional landscape. Despite having relevant skills and training, many have had their studies and careers disrupted either by conflict, or simply by lacking the profile and networks needed to restart their careers in a new country. With limited resources and time, combined with the intensive pace and diverse student backgrounds, the program faces many challenges that threaten its success. To mitigate these challenges, an agile and adaptive approach was adopted that employs TEL techniques and pedagogical concepts to ensure the program is continuously improving via short iterations and tight feedback loops. The program has just finished its third offering and has continuously improved through weekly collection of knowledge, confidence, and experience data that guide interventions and reactions as they are needed. The experience, process, and model presented here may inspire and benefit other courses with similar profiles and challenges.

  • 14.
    Holmqvist, Carl
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Opinion analysis of microblogs for stock market prediction2018Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    This degree project investigates if a company’s stock price development can be predicted using the general opinion expressed in tweets about the company. The project starts off with the model from a previous project and then tries to improve the results using state-of-the-art neural network sentiment analysis and more tweet data. This project also attempts to perform hourly predictions along with daily predictions in order to investigate the method further.

    The results show a decrease in accuracy compared to the previous project. The results also indicate that the neural network sentiment analysis improves the accuracy of the stock price development when compared to the baseline model under comparable conditions.

  • 15. Iatropoulos, G.
    et al.
    Herman, Pawel
    KTH, School of Electrical Engineering and Computer Science (EECS), Computational Science and Technology (CST).
    Lansner, Anders
    KTH, School of Electrical Engineering and Computer Science (EECS), Computational Science and Technology (CST).
    Karlgren, Jussi
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS. Gavagai, Slussplan 9, Stockholm, Sweden.
    Larsson, M.
    Olofsson, J. K.
    The language of smell: Connecting linguistic and psychophysical properties of odor descriptors2018In: Cognition, ISSN 0010-0277, E-ISSN 1873-7838, Vol. 178, p. 37-49Article in journal (Refereed)
    Abstract [en]

    The olfactory sense is a particularly challenging domain for cognitive science investigations of perception, memory, and language. Although many studies show that odors often are difficult to describe verbally, little is known about the associations between olfactory percepts and the words that describe them. Quantitative models of how odor experiences are described in natural language are therefore needed to understand how odors are perceived and communicated. In this study, we develop a computational method to characterize the olfaction-related semantic content of words in a large text corpus of internet sites in English. We introduce two new metrics: olfactory association index (OAI, how strongly a word is associated with olfaction) and olfactory specificity index (OSI, how specific a word is in its description of odors). We validate the OAI and OSI metrics using psychophysical datasets by showing that terms with high OAI have high ratings of perceived olfactory association and are used to describe highly familiar odors. In contrast, terms with high OSI have high inter-individual consistency in how they are applied to odors. Finally, we analyze Dravnieks's (1985) dataset of odor ratings in terms of OAI and OSI. This analysis reveals that terms that are used broadly (applied often but with moderate ratings) tend to be olfaction-unrelated and abstract (e.g., “heavy” or “light”; low OAI and low OSI) while descriptors that are used selectively (applied seldom but with high ratings) tend to be olfaction-related (e.g., “vanilla” or “licorice”; high OAI). Thus, OAI and OSI provide behaviorally meaningful information about olfactory language. These statistical tools are useful for future studies of olfactory perception and cognition, and might help integrate research on odor perception, neuroimaging, and corpus-based linguistic models of semantic organization.

  • 16. Ive, J.
    et al.
    Viani, N.
    Chandran, D.
    Bittar, A.
    Velupillai, Sumithra
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS. King's College London, IoPPN, London, SE5 8AF, United Kingdom.
    KCL-Health-NLP@CLEF eHealth 2018 Task 1: ICD-10 coding of French and Italian death certificates with character-level convolutional neural networks2018In: CEUR Workshop Proceedings, CEUR-WS , 2018, Vol. 2125Conference paper (Refereed)
    Abstract [en]

    In this paper we describe the participation of the KCL-Health-NLP team in the CLEF eHealth 2018 lab, specifically Task 1: Multilingual Information Extraction-ICD10 coding. The task involves the automatic coding of causes of death in death certificates in French, Italian and Hungarian according to the ICD-10 taxonomy. Choosing to work on the two Romance languages, we treated the task as a sequence-to-sequence prediction problem. Our system has an encoder-decoder architecture, with convolutional neural networks based on character em-beddings as encoders and recurrent neural network decoders. Our hypothesis was that a character-level representation would allow our model to generalise across two genealogically related languages. Results obtained by pre-training our Italian model on the French data set confirmed this intuition. We also explored the impact of character-level features extracted from dictionary-matched ICD codes. We obtained F-measures of 0.72/0.64 and 0.78 on the French aligned/raw and Italian raw internal test data, respectively. On the blind test set released by the task organisers, our top results were 0.65/0.52 and 0.69 F-measure, respectively.

  • 17.
    Josefsson, Pernilla
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Media Technology and Interaction Design, MID.
    Baltatzis, Alexander
    KTH, School of Electrical Engineering and Computer Science (EECS), Media Technology and Interaction Design, MID.
    Bälter, Olof
    KTH, School of Electrical Engineering and Computer Science (EECS), Media Technology and Interaction Design, MID.
    Enoksson, Fredrik
    KTH, School of Industrial Engineering and Management (ITM).
    Hedin, Björn
    KTH, School of Electrical Engineering and Computer Science (EECS), Media Technology and Interaction Design, MID.
    Riese, Emma
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    DRIVERS AND BARRIERS FOR PROMOTING TECHNOLOGY ENHANCED LEARNING IN HIGHER EDUCATION2018In: 12TH INTERNATIONAL TECHNOLOGY, EDUCATION AND DEVELOPMENT CONFERENCE (INTED) / [ed] Chova, LG Martinez, AL Torres, IC, IATED-INT ASSOC TECHNOLOGY EDUCATION & DEVELOPMENT , 2018, p. 4576-4584Conference paper (Refereed)
    Abstract [en]

    The paper presents a study were drivers and barriers for increased use of Technology Enhanced Learning in higher education were identified. The method included focus groups with Faculty Pedagogical Developers at KTH Royal Institute of Technology, followed by a Force Field Analysis. Ten drivers and ten barriers were identified, and are presented in this paper. The most significant drivers found were: collegial discussions, increased automatization, Technology enhanced learning support for the teachers (to assist exploration), tech savvy students and engagement among faculty. The most significant barriers identified were: unclear return on time investment, insufficient funding for purchases and lack of central decisions. The analysis also revealed that some drivers and barriers could act both ways. One example is locally developed systems which are understood to be drivers when it comes to solving (local) problems and encouraging experimentation with IT systems, but when these local systems are cancelled due to lack of funding, or for example replaced by centralized systems, they discourage use and development. The findings constitute a foundation for future discussions about change processes to increase utilization of technology enhanced learning in higher education.

  • 18.
    Karlgren, Jussi
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS. Gavagai, Stockholm, Sweden.
    Esposito, L.
    Gratton, C.
    Kanerva, P.
    Authorship profiling without using topical information: Notebook for PAN at CLEF 20182018In: CLEF 2018 Working Notes, CEUR-WS , 2018, Vol. 2125Conference paper (Refereed)
    Abstract [en]

    This paper describes an experiment made for the PAN 2018 shared task on author profiling. The task is to distinguish female from male authors of microblog posts published on Twitter using no extraneous information except what is in the posts; this experiment focusses on using non-topical information from the posts, rather than gender differences in referential content.

  • 19.
    Karlgren, Jussi
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Kanerva, P.
    Hyperdimensional utterance spaces2018In: CEUR Workshop Proceedings, CEUR-WS , 2018, Vol. 2167, p. 29-35Conference paper (Refereed)
    Abstract [en]

    Human language has a large and varying number of features, both lexical items and constructions, which interact to represent various aspects of communicative information. High-dimensional semantic spaces have proven useful and effective for aggregating and processing lexical information for many language processing tasks. This paper describes a hyperdimensional processing model for language data, a straightforward extension of models previously used for words to handling utterance or text level information. A hyperdimensional model is able to represent a broad range of linguistic and extra-linguistic features in a common integral framework which is suitable as a bridge between symbolic and continuous representations, as an encoding scheme for symbolic information and as a basis for feature space exploration. This paper provides an overview of the framework and an example of how it is used in a pilot experiment.

  • 20.
    Khosrowjerdi, Hojat
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Meinke, Karl
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Rasmusson, Andreas
    Scania CV AB, S-15187 Sodertalje, Sweden..
    Virtualized-Fault Injection Testing: a Machine Learning Approach2018In: 2018 IEEE 11TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST), IEEE , 2018, p. 297-308Conference paper (Refereed)
    Abstract [en]

    We introduce a new methodology for virtualized fault injection testing of safety critical embedded systems. This approach fully automates the key steps of test case generation, fault injection and verdict construction. We use machine learning to reverse engineer models of the system under test. We use model checking to generate test verdicts with respect to safety requirements formalised in temporal logic. We exemplify our approach by implementing a tool chain based on integrating the QEMU hardware emulator, the GNU debugger GDB and the LBTest requirements testing tool. This tool chain is then evaluated on two industrial safety critical applications from the automotive sector.

  • 21.
    Kitamura, T.
    et al.
    Japan.
    Maissonneuve, Q.
    Japan.
    Choi, E. -H
    Japan.
    Artho, Cyrille
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Gargantini, A.
    Italy.
    Optimal Test Suite Generation for Modified Condition Decision Coverage Using SAT Solving2018In: 37th International Conference on Computer Safety, Reliability and Security, SAFECOMP 2018, Springer, 2018, p. 123-138Conference paper (Refereed)
    Abstract [en]

    Boolean expressions occur frequently in descriptions of computer systems, but they tend to be complex and error-prone in complex systems. The modified condition decision coverage (MCDC) criterion in system testing is an important testing technique for Boolean expression, as its usage mandated by safety standards such as DO-178 [1] (avionics) and ISO26262 [2] (automotive). In this paper, we develop an algorithm to generate optimal MCDC test suites for Boolean expressions. Our algorithm is based on SAT solving and generates minimal MCDC test suites. Experiments on a real-world avionics system confirm that the technique can construct minimal MCDC test suites within reasonable times, and improves significantly upon prior techniques.

  • 22. Kozma, László
    et al.
    Saranurak, Thatchaphol
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Smooth Heaps and a Dual View of Self-adjusting Data Structures2018In: Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, ACM , 2018, p. 801-814Conference paper (Refereed)
    Abstract [en]

    We present a new connection between self-adjusting binary search trees (BSTs) and heaps, two fundamental, extensively studied, and practically relevant families of data structures (Allen, Munro, 1978; Sleator, Tarjan, 1983; Fredman, Sedgewick, Sleator, Tarjan, 1986; Wilber, 1989; Fredman, 1999; Iacono, Özkan, 2014). Roughly speaking, we map an arbitrary heap algorithm within a broad and natural model, to a corresponding BST algorithm with the same cost on a dual sequence of operations (i.e. the same sequence with the roles of time and key-space switched). This is the first general transformation between the two families of data structures. There is a rich theory of dynamic optimality for BSTs (i.e. the theory of competitiveness between BST algorithms). The lack of an analogous theory for heaps has been noted in the literature (e.g. Pettie; 2005, 2008). Through our connection, we transfer all instance-specific lower bounds known for BSTs to a general model of heaps, initiating a theory of dynamic optimality for heaps. On the algorithmic side, we obtain a new, simple and efficient heap algorithm, which we call the smooth heap. We show the smooth heap to be the heap-counterpart of Greedy, the BST algorithm with the strongest proven and conjectured properties from the literature, widely believed to be instance-optimal (Lucas, 1988; Munro, 2000; Demaine et al., 2009). Assuming the optimality of Greedy, the smooth heap is also optimal within our model of heap algorithms. Intriguingly, the smooth heap, although derived from a non-practical BST algorithm, is simple and easy to implement (e.g. it stores no auxiliary data besides the keys and tree pointers). It can be seen as a variation on the popular pairing heap data structure, extending it with a “power-of-two-choices” type of heuristic. For the smooth heap we obtain instance-specific upper bounds, with applications in adaptive sorting, and we see it as a promising candidate for the long-standing question of a simpler alternative to Fibonacci heaps. The paper is dedicated to Raimund Seidel on occasion of his sixtieth birthday.

  • 23.
    Lundberg, Didrik
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Provably Sound and Secure Automatic Proving and Generation of Verification Conditions2018Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. This thesis presents a proof procedure to efficiently generate a theorem stating the weakest precondition for a program to terminate successfully in a state upon which a certain postcondition is placed. Specifically, the Poly/ML implementation of the SML metalanguage is used to generate a theorem in the HOL4 interactive theorem prover regarding the properties of a program written in BIR, an abstract intermediate representation of machine code used in the PROSPER project.

  • 24. Martinez, M.
    et al.
    Monperrus, Martin
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Ultra-large repair search space with automatically mined templates: The cardumen mode of astor2018In: 10th International Symposium on Search-Based Software Engineering, SSBSE 2018, Springer, 2018, Vol. 11036, p. 65-86Conference paper (Refereed)
    Abstract [en]

    Astor is a program repair library which has different modes. In this paper, we present the Cardumen mode of Astor, a repair approach based mined templates that has an ultra-large search space. We evaluate the capacity of Cardumen to discover test-suite adequate patches (aka plausible patches) over the 356 real bugs from Defects4J [11]. Cardumen finds 8935 patches over 77 bugs of Defects4J. This is the largest number of automatically synthesized patches ever reported, all patches being available in an open-science repository. Moreover, Cardumen identifies 8 unique patches, that are patches for Defects4J bugs that were never repaired in the whole history of program repair.

  • 25.
    Meinke, Karl
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Bennaceur, A.
    Machine learning for software engineering: Models, methods, and applications2018In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, IEEE Computer Society, 2018, p. 548-549Conference paper (Refereed)
    Abstract [en]

    Machine Learning (ML) is the discipline that studies methods for automatically inferring models from data. Machine learning has been successfully applied in many areas of software engineering ranging from behaviour extraction, to testing, to bug fixing. Many more applications are yet be defined. However, a better understanding of ML methods, their assumptions and guarantees would help software engineers adopt and identify the appropriate methods for their desired applications. We argue that this choice can be guided by the models one seeks to infer. In this technical briefing, we review and reflect on the applications of ML for software engineering organised according to the models they produce and the methods they use. We introduce the principles of ML, give an overview of some key methods, and present examples of areas of software engineering benefiting from ML. We also discuss the open challenges for reaching the full potential of ML for software engineering and how ML can benefit from software engineering methods.

  • 26.
    Mukhopadhyay, Sagnik
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Radhakrishnan, Jaykumar
    Tata Inst Fundamental Res, Bombay, Maharashtra, India..
    Sanyal, Swagato
    IIT Kharagpur, Dept Comp Sci & Engn, Kharagpur, W Bengal, India..
    Separation Between Deterministic and Randomized Query Complexity2018In: SIAM journal on computing (Print), ISSN 0097-5397, E-ISSN 1095-7111, Vol. 47, no 4, p. 1644-1666Article in journal (Refereed)
    Abstract [en]

    Saks and Wigderson 27th FOGS, IEEE Computer Society, as Alamitos, CA, 1986, pp. 29-38] conjectured that R-0(f) = Omega (D(f)(0.753...)) for all Boolean functions f, here R-0 denotes the randomized complexity and D denotes 10 determinist is query CCATI p1exit;,yr. We,show t hat for the pointer function GPW(rxs) defined by Goos. Pitassi, arid Watson [in Proceedings of the 56th FOCS, IEEE, Piscataway, NJ, 2015, pp. 1077-1088] the following hold: s) s) and (b) R-1(GPW(rxs)) = Irs), cyhere R1 denotes the randomized one-sided error query complexity. These results imply that (i) R-0(GPW(s2xs)) = O(D(GPW(s2xs))2/3) t hereby refuting the; conjecture of Saks and Wigdorson, and (ii) R-1 (GPW(sxs))- O(R-0(GPW(sxs))(2/3)), thereby providing a polynomial separation between the randomized zero -error and one-sided error query complexity measures.

  • 27. Nemati, H.
    et al.
    Baumann, Christoph
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Formal verification of integrity-Preserving countermeasures against cache storage side-channels2018In: 7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Springer Verlag , 2018, p. 109-133Conference paper (Refereed)
    Abstract [en]

    Formal verification of systems-level software such as hypervisors and operating systems can enhance system trustworthiness. However, without taking low level features like caches into account the verification may become unsound. While this is a well-known fact w.r.t. timing leaks, few works have addressed latent cache storage side-channels, whose effects are not limited to information leakage. We present a verification methodology to analyse soundness of countermeasures used to neutralise these channels. We apply the proposed methodology to existing countermeasures, showing that they allow to restore integrity of the system. We decompose the proof effort into verification conditions that allow for an easy adaption of our strategy to various software and hardware platforms. As case study, we extend the verification of an existing hypervisor whose integrity can be tampered using cache storage channels. We used the HOL4 theorem prover to validate our security analysis, applying the verification methodology to a generic hardware model. 

  • 28. Pandurangan, G.
    et al.
    Robinson, P.
    Scquizzato, Michele
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    On the distributed complexity of large-scale graph computations2018In: SPAA '18 Proceedings of the 30th on Symposium on Parallelism in Algorithms and Architectures, Association for Computing Machinery (ACM), 2018, p. 405-414Conference paper (Refereed)
    Abstract [en]

    Motivated by the increasing need to understand the distributed algorithmic foundations of large-scale graph computations, we study some fundamental graph problems in a message-passing model for distributed computing where k 2 machines jointly perform computations on graphs with n nodes (typically, n ≫ k). The input graph is assumed to be initially randomly partitioned among the k machines, a common implementation in many real-world systems. Communication is point-to-point, and the goal is to minimize the number of communication rounds of the computation.

  • 29. Rauf, I.
    et al.
    Vistbakka, I.
    Troubitsyna, Elena
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Formal Verification of Stateful Services with REST APIs Using Event-B2018In: Proceedings - 2018 IEEE International Conference on Web Services, ICWS 2018 - Part of the 2018 IEEE World Congress on Services, Institute of Electrical and Electronics Engineers Inc. , 2018, p. 131-138Conference paper (Refereed)
    Abstract [en]

    REST APIs are being increasingly used in the industry including their application in safety-critical domain and in the IoT world. They offer basic CRUD (create, retrieve, update and delete) interfaces. However, REST APIs can be used to build services with more advanced scenarios. Developing such services with REST constraints requires rigorous approaches that are capable of creating services that can be trusted for their behavior. In this work, we present an approach based on formal verification technique for a development of REST services using Event-B. We focus on deriving a correct system architecture by refinement and consistency verification of service design models. We illustrate our approach on a Hotel Reservation System. 

  • 30.
    Saranurak, Thatchaphol
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Dynamic algorithms: new worst-case and instance-optimal bounds via new connections2018Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    This thesis studies a series of questions about dynamic algorithms which are algorithms for quickly maintaining some information of an input data undergoing a sequence of updates. The first question asks \emph{how small the update time for handling each update can be} for each dynamic problem. To obtain fast algorithms, several relaxations are often used including allowing amortized update time, allowing randomization, or even assuming an oblivious adversary. Hence, the second question asks \emph{whether these relaxations and assumptions can be removed} without sacrificing the speed. Some dynamic problems are successfully solved by fast dynamic algorithms without any relaxation. The guarantee of such algorithms, however, is for a worst-case scenario. This leads to the last question which asks for \emph{an algorithm whose cost is nearly optimal for every scenario}, namely an instance-optimal algorithm. This thesis shows new progress on all three questions.

    For the first question, we give two frameworks for showing the inherent limitations of fast dynamic algorithms. First, we propose a conjecture called the Online Boolean Matrix-vector Multiplication Conjecture (OMv). Assuming this conjecture, we obtain new \emph{tight} conditional lower bounds of update time for more than ten dynamic problems even when algorithms are allowed to have large polynomial preprocessing time. Second, we establish the first analogue of ``NP-completeness'' for dynamic problems, and show that many natural problems are ``NP-hard'' in the dynamic setting. This hardness result is based on the hardness of all problems in a huge class that includes a number of natural and hard dynamic problems. All previous conditional lower bounds for dynamic problems are based on hardness of specific problems/conjectures.

    For the second question, we give an algorithm for maintaining a minimum spanning forest in an $n$-node graph undergoing edge insertions and deletions using $n^{o(1)}$ worst-case update time with high probability. This significantly improves the long-standing $O(\sqrt{n})$ bound by {[}Frederickson STOC'83, Eppstein, Galil, Italiano and Nissenzweig FOCS'92{]}. Previously, a spanning forest (possibly not minimum) can be maintained in polylogarithmic update time if either amortized update is allowed or an oblivious adversary is assumed. Therefore, our work shows how to eliminate these relaxations without slowing down updates too much.

    For the last question, we show two main contributions on the theory of instance-optimal dynamic algorithms. First, we use the forbidden submatrix theory from combinatorics to show that a binary search tree (BST) algorithm called \emph{Greedy} has almost optimal cost when its input \emph{avoids a pattern}. This is a significant progress towards the Traversal Conjecture {[}Sleator and Tarjan JACM'85{]} and its generalization. Second, we initialize the theory of instance optimality of heaps by showing a general transformation between BSTs and heaps and then transferring the rich analogous theory of BSTs to heaps. Via the connection, we discover a new heap, called the \emph{smooth heap}, which is very simple to implement, yet inherits most guarantees from BST literature on being instance-optimal on various kinds of inputs. The common approach behind all our results is about making new connections between dynamic algorithms and other fields including fine-grained and classical complexity theory, approximation algorithms for graph partitioning, local clustering algorithms, and forbidden submatrix theory.

  • 31.
    Schmid, Stefan
    et al.
    Univ Vienna, Fac Comp Sci, Wahringer Str 29, AT-1090 Vienna, Austria..
    Pandurangan, Gopal
    Univ Houston, Dept Comp Sci, Houston, TX 77204 USA..
    Robinson, Peter
    McMaster Univ, Dept Comp & Software, Hamilton, ON, Canada..
    Scquizzato, Michele
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    The Distributed Minimum Spanning Tree Problem2018In: Bulletin of the European Association for Theoretical Computer Science, ISSN 0252-9742, no 125, p. 51-80Article in journal (Refereed)
    Abstract [en]

    This article surveys the distributed minimum spanning tree (MST) problem, a central and one of the most studied problems in distributed computing. In this problem, we are given a network, represented as a weighted graph G = (v, E), and the nodes in the network communicate by message passing via the edges of G with the goal of constructing an MST of G in a distributed fashion, i.e., each node should identify the MST edges incident to itself. This article summarizes the long line of research in designing efficient distributed algorithms and showing lower bounds for the distributed MST problem, including the most recent developments which have focused on algorithms that are simultaneously round- and message-optimal.

  • 32.
    Stewart, R.
    et al.
    United Kingdom.
    Jackson, R.
    United Kingdom.
    Patel, R.
    united Kingdom.
    Velupillai, Sumithra
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Gkotsis, G.
    United Kingdom.
    Hoyle, D.
    United Kingdom.
    Knowledge discovery for Deep Phenotyping serious mental illness from Electronic Mental Health records2018In: F1000 Research, E-ISSN 2046-1402, Vol. 7, article id 210Article in journal (Refereed)
    Abstract [en]

    Background: Deep Phenotyping is the precise and comprehensive analysis of phenotypic features in which the individual components of the phenotype are observed and described. In UK mental health clinical practice, most clinically relevant information is recorded as free text in the Electronic Health Record, and offers a granularity of information beyond what is expressed in most medical knowledge bases. The SNOMED CT nomenclature potentially offers the means to model such information at scale, yet given a sufficiently large body of clinical text collected over many years, it is difficult to identify the language that clinicians favour to express concepts. Methods: By utilising a large corpus of healthcare data, we sought to make use of semantic modelling and clustering techniques to represent the relationship between the clinical vocabulary of internationally recognised SMI symptoms and the preferred language used by clinicians within a care setting. We explore how such models can be used for discovering novel vocabulary relevant to the task of phenotyping Serious Mental Illness (SMI) with only a small amount of prior knowledge. Results: 20 403 terms were derived and curated via a two stage methodology. The list was reduced to 557 putative concepts based on eliminating redundant information content. These were then organised into 9 distinct categories pertaining to different aspects of psychiatric assessment. 235 concepts were found to be expressions of putative clinical significance. Of these, 53 were identified having novel synonymy with existing SNOMED CT concepts. 106 had no mapping to SNOMED CT. Conclusions: We demonstrate a scalable approach to discovering new concepts of SMI symptomatology based on real-world clinical observation. Such approaches may offer the opportunity to consider broader manifestations of SMI symptomatology than is typically assessed via current diagnostic frameworks, and create the potential for enhancing nomenclatures such as SNOMED CT based on real-world expressions.

  • 33.
    Swernofsky, Joseph
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Tensor rank is hard to approximate2018In: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2018, article id 26Conference paper (Refereed)
    Abstract [en]

    We prove that approximating the rank of a 3-tensor to within a factor of 1+1/1852-δ, for any δ > 0, is NP-hard over any field. We do this via reduction from bounded occurrence 2-SAT.

  • 34. Urli, S.
    et al.
    Yu, Z.
    Seinturier, L.
    Monperrus, Martin
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    How to design a program repair bot?: Insights from the repairnator project2018In: Proceedings - International Conference on Software Engineering, IEEE Computer Society, 2018, p. 95-104Conference paper (Refereed)
    Abstract [en]

    Program repair research has made tremendous progress over the last few years, and software development bots are now being invented to help developers gain productivity. In this paper, we investigate the concept of a "program repair bot" and present Repairnator. The Repairnator bot is an autonomous agent that constantly monitors test failures, reproduces bugs, and runs program repair tools against each reproduced bug. If a patch is found, Repairnator bot reports it to the developers. At the time of writing, Repairnator uses three different program repair systems and has been operating since February 2017. In total, it has studied 11 523 test failures over 1 609 open-source software projects hosted on GitHub, and has generated patches for 15 different bugs. Over months, we hit a number of hard technical challenges and had to make various design and engineering decisions. This gives us a unique experience in this area. In this paper, we reflect upon Repairnator in order to share this knowledge with the automatic program repair community.

  • 35. Vahabi, Maryam
    et al.
    Faragardi, Hamid Reza
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Fotohi, Hossein
    An analytical model for deploying mobile sinks in industrial Internet of Things2018In: 2018 IEEE Wireless Communications and Networking Conference Workshops (WCNCW), IEEE Press, 2018Conference paper (Refereed)
    Abstract [en]

    Nowadays, the Industrial Internet of Things (IIoT) has the potential to be implemented in factories and supply chains to improve manufacturing efficiency. It is becoming more common to use mobile robots in such factories for further improvements. Adding data collection capability to the mobile robots would realize the mobile sink deployment in future factories. As it is important to reduce the deployment cost, we are aiming at a network with minimum number of mobile sinks while ensuring network reliability and timeliness. In this paper, we analytically model a given trajectory for the motion of mobile sinks and the routing of mobile sinks along the trajectory in an IIoT system. We introduce an optimization problem in the form of Integer Linear Programming (ILP) to specify the minimum number of required mobile sinks to reduce deployment cost of an IIoT system, and also to identify the routing of multiple mobile sinks along a given trajectory. The proposed ILP model can be solved by several existing off-the-shelf ILP-solvers.

  • 36.
    Viberg, Olga
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Media Technology and Interaction Design, MID.
    Bälter, Olof
    KTH, School of Electrical Engineering and Computer Science (EECS), Media Technology and Interaction Design, MID.
    Hedin, Björn
    KTH, School of Electrical Engineering and Computer Science (EECS), Media Technology and Interaction Design, MID.
    Riese, Emma
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Mavroudi, Anna
    KTH, School of Electrical Engineering and Computer Science (EECS), Media Technology and Interaction Design, MID.
    Faculty pedagogical developers as enablers of technology‐enhanced learning2018In: British Journal of Educational Technology, ISSN 0007-1013, E-ISSN 1467-8535, p. 1-14Article in journal (Refereed)
    Abstract [en]

    As the integration of digital technologies in higher education continues to increase, there is a need to understand how to best support university teachers as designers of technology‐enhanced learning (TEL) in order to support students to achieve academic success. In this study, we have examined the Faculty Pedagogical Developer Initiative at KTH Royal Institute of Technology in Sweden, an innovative project to support a bottom‐up change process of teachers as designers of TEL, with the intent to strengthen the professional pedagogical development for the faculty. Data were collected from interviews and official documents. Actor–network theory was applied for the analysis. The results suggest that the initiative stimulated both practical implementation of digital technology in educational programmes and also spurred a debate about teachers as designers of TEL between these pedagogical developers and other teachers across different schools and subjects at KTH. However, there are important social, organisational and technical challenges that should be considered when developing support for university teachers as designers of TEL. This paper concludes that this process requires a deep understanding of four interrelated elements: information, technology, organisation and social arrangements.

  • 37. Vinyals, M.
    et al.
    Elffers, Jan
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Giráldez Crú, Jesus
    KTH.
    Gocht, Stephan
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Nordström, Jakob
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving2018In: 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Springer, 2018, Vol. 10929, p. 292-310Conference paper (Refereed)
    Abstract [en]

    We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflict-driven pseudo-Boolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that so-called saturation is used instead of division. It is known that on CNF inputs cutting planes with cancelling addition and saturation is essentially just resolution. We show that even if general addition is allowed, this proof system is still polynomially simulated by resolution with respect to proof size as long as coefficients are polynomially bounded. As a further way of delineating the proof power of subsystems of CP, we propose to study a number of easy (but tricky) instances of problems in NP. Most of the formulas we consider have short and simple tree-like proofs in general CP, but the restricted subsystems seem to reveal a much more varied landscape. Although we are not able to formally establish separations between different subsystems of CP—which would require major technical breakthroughs in proof complexity—these formulas appear to be good candidates for obtaining such separations. We believe that a closer study of these benchmarks is a promising approach for shedding more light on the reasoning power of pseudo-Boolean solvers.

  • 38. Vistbakka, I.
    et al.
    Barash, M.
    Troubitsyna, Elena
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS. Åbo Akademi University, Turku, Finland.
    Towards creating a DSL facilitating modelling of dynamic access control in event-B2018In: 6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018, Springer, 2018, Vol. 10817, p. 386-391Conference paper (Refereed)
    Abstract [en]

    Role-Based Access Control (RBAC) is a popular authorization model used to manage resource-access constraints in a wide range of systems. The standard RBAC framework adopts a static, state-independent approach to define the access rights to the system resources. It is often insufficient for correct implementation of the desired functionality and should be augmented with the dynamic, i.e., a state-dependant view on the access control. In this paper, we present a work in progress on creating a domain-specific language and the tool support for modelling and verification of dynamic RBAC. They support a tabular representation of the static RBAC constraints together with the graphical model of the scenarios and enable an automated translation of them into an Event-B model.

  • 39.
    Zhang, Long
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
    Morin, Brice
    Haller, Philipp
    Baudry, Benoit
    Monperrus, Martin
    A Chaos Engineering System for Live Analysis and Falsification of Exception-handling in the JVMManuscript (preprint) (Other academic)
    Abstract [en]

    Software systems contain resilience code to handle those failures and unexpected events happening in production. It is essential for developers to understand and assess the resilience of their systems. Chaos engineering is a technology that aims at assessing resilience and uncovering weaknesses by actively injecting perturbations in production. In this paper, we propose a novel design and implementation of a chaos engineering system in Java called CHAOSMACHINE. It provides a unique and actionable analysis on exception-handling capabilities in production, at the level of try-catch blocks. To evaluate our approach, we have deployed CHAOSMACHINE on top of 3 large-scale and well-known Java applications totaling 630k lines of code. Our results show that CHAOSMACHINE reveals both strengths and weaknesses of the resilience code of a software system at the level of exception handling.

1 - 39 of 39
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf