Microsoft Technology Licensing, LLC

Shuvendu K Lahiri

Neelakantan Sundaresan

Thomas J Ball

Shao Kun Deng

Xiaoyu Liu

Xin Shi

Matthew Glenn Jin

Ranveer Chandra

Mark Alan Champion

Alexey Svyatkovskiy

Nikolaj Skallerud Bjorner

Yuan Yu

Madanlal S Musuvathi

Todd Douglas Mytkowicz

Manuel Alfred Fahndrich

Shaz Qadeer

Sam Sarmast

Patrice Godefroid

Christian Alma Bird

Jacek Andrzej Czerwonka

Jeremy P Condit

Chris Hawblitzel

Suresh Thummalapenta

Akash Lal

Francesco Logozzo

Sam Blackshear

Cindy Rubio-Gonzalez

Saurabh Joshi

Jinghao Shi

August Shi

Christian Bird

Manuel Fahndrich

An automated system for resolving program merges uses neural transformers with attention. In one aspect, a neural encoder transformer model is trained from developer-resolved merge conflicts to learn to predict a resolution strategy that aids a developer in constructing a merged program. In a second aspect, a neural decoder transformer model is trained on the syntax and semantics of different source code programming languages to predict a merge resolution consisting of interleaved lines of source code from programs A, B, or O, where programs A and B contain changes to code base O.

Automated merge conflict resolution with transformers

Language interoperability between source code programs not compatible with an interprocedural static code analyzer is achieved through language-independent representations of the programs. The source code programs are transformed into respective intermediate language instructions from which a language-independent control flow graph and a language-independent type environment is created. A program compatible with the interprocedural static code analyzer is generated from the language-independent control flow graph and the language-independent type environment in order to utilize the interprocedural static code analyzer to detect memory safety faults.

Language interoperability to automate code analysis

The factorization of test components when performing component-level regression testing in iterative builds of a computing system that consists of many working components. Performance metrics for test components are maintained across multiple builds of the computing program. To perform factorization, multiple factorings of a test component are identified and evaluated until a suitable improvement in the maintained performance metric for each corresponding test component is achieved (e.g., via simulation). This may be performed, across multiple of the test components. This process may be iterated through such that the set of test components being factored and evaluated in a subsequent iteration may in fact be a test component created by factorization in a prior iteration. The net result is that the factorization achieves improvement in performance metrics of the test components.

Test components factorization in a build system

Described herein are technologies pertaining to semantic baselining. Correctness conditions of a baseline program are inferred based upon a first static analysis undertaken over the baseline program. The correctness conditions are subsequently inserted into a revision to the baseline program. When a second static analysis is undertaken over the revised program with the correctness conditions inserted therein, warnings inherited from the baseline program are suppressed, while warnings caused by revisions are surfaced to a developer.

Semantic baselining

The description relates to wireless protocol verification. One example can obtain information relating to a wireless protocol and receive information relating to wireless communications associated with a wireless device. The example can compare the wireless communications with the wireless protocol and generate a verification report that conveys whether the wireless communications comply with the wireless protocol.

Verification of a wireless protocol implementation

To overcome the difficulties inherent in traditional compiler validating methods, a new technique is herein provided for validating compiler output via program verification. In one embodiment, this technique is implemented as an automated tool that merges both a source program and the compiler-generated target program into a single (intermediate) program. An automated program verifier is then applied to the merged program. Subsequently, the program verifier compares the source and target programs and determines if the programs are semantically equivalent.

Compiler validation via program verification

This document describes a unified type checker and property checker for a low level program's heap and its types. The type checker can use the full power of the property checker to express and verify subtle, program specific type and memory safety invariants well beyond what the native low level program system can check. Meanwhile, the property checker can rely on the type checker to provide structure and disambiguation for the program's heap, enabling more concise and more powerful type-based specifications. This approach makes use of a fully automated Satisfiability Modulo Theories (SMT) solver and a decision procedure for checking type safety, which means that the programmer's only duty is to provide high-level type and property annotations as part of the original program's source.

Unifying type checking and property checking for low level programs

The claimed subject matter provides a method for performing a static analysis of concurrent programs. The method includes determining that a static analysis of the first concurrent program generates a warning for an input. The method also includes determining whether a static analysis of the second concurrent program generates the warning for the input. The method further includes removing the warning if the static analysis of the second concurrent program generates the warning.

Reducing false alarms for static analysis of concurrent programs

Concepts and technologies are described herein for incremental compositional dynamic test generation. The concepts and technologies described herein are used to increase the code coverage and security vulnerability identification abilities of testing applications and devices, without significantly increasing, and in some cases decreasing, computational and time costs associated with the testing. Test summaries that describe how code is tested by a test engine are generated and stored during testing of code. These test summaries can be evaluated when additional iterations or versions of the code are tested. If functions corresponding to the test summaries are unchanged from, or logically equivalent to, a version of the function previously tested, the test summary may be used when testing the new version of the code.

Incremental compositional dynamic test generation

A library or application is selected comprising one or more functions or methods. An interesting subset of the functions or methods is created. A plurality of multi-threaded test cases are generated from the subset of interesting functions or methods, with each test case comprising a unique pair or triple of functions or methods from the subset. The resulting set of test cases may then be filtered of thread safe test cases using static analysis techniques. The filtered set of test cases is then used as an input to a specialized application that executes each of the multi-threaded test cases to detect atomicity violations and race conditions. The results of the execution of each of the test cases by the specialized application are then aggregated and presented to a user or administrator in a report, for example.

Automatic and systematic detection of race conditions and atomicity violations

A computer implemented method for solving linear arithmetic constraints that combines a solver for difference constraints with a general linear arithmetic constraint solver. When used to solve sparse linear arithmetic constraints, the time and space complexity of the process is determined by the difference constraint component.

Computer implemented methods for solving difference and non-difference linear constraints

Predicate abstraction techniques and tools. Using symbolic decision procedures, predicate abstractions for computer programs are generated based on a set of predicates representing observations of expected behavior of the program. The set of predicates may be generated by an automatic program analysis tool or may be provided a user based on the user's observations. The predicate abstraction process may employ binary decision diagrams. Two or more symbolic decision procedures (e.g., for different kinds of program logic) can be combined to form a combined symbolic decision procedure to be used for predicate abstraction. A data structure can be used to track derived predicates during predicate abstraction.

Growing community of inventors

Issaquah, WA, United States of America

Shuvendu K Lahiri